\module Paths.Meta

Rewriting metas

Metas rewrite, rewriteI, and rewriteF work just like the rewriting mechanism in other languages, such as Coq or Idris (in Agda, rewrite is allowed only in the LHS of a clause, so it’s different).

• rewrite p t : T where p : a = b replaces occurrences of a in T with a variable x obtaining a type T[x/a] and returns transportInv (\lam x => T[x/a]) p t. Note that T is the expected type from the context, not the type of t. When the expected type is unknown, the type of t will be used instead of T.
• rewriteF is like rewrite but it enforces to use the type of t instead of the expected type.
• rewriteI p t is equivalent to rewrite (inv p) t.

To any of the metas above it is possible to add specification of numbers of occurrences. For example, rewrite {i1, i2, … ik} p t : T rewrites only occurrences with numbers i1, i2, … ik where occurrence ij is the number of occurrence after all previous occurrences have been replaced.

Examples:

\import Function.Meta
\import Paths.Meta
\import Data.List

\lemma +-assoc (a b c : Nat) : a + b + c = a + (b + c) \elim c
  | 0 => idp
  | suc c => rewrite (+-assoc a b c) idp

\lemma +-comm-rw (a b : Nat) : a + b = b + a
  | 0, 0 => idp
  | 0, suc b => rewrite (+-comm-rw 0 b) idp
  | suc a, 0 => rewriteI (+-comm-rw a 0) idp
  | suc a, suc b => rewrite (+-comm-rw $ suc a) $
       rewriteI (+-comm-rw a b) $ rewriteI (+-comm-rw a $ suc b) idp

\lemma test1 (x y : Nat) (p : x = 0) (q : 0 = y) : x = y => rewrite p q

\lemma test2 (x y : Nat) (p : 0 = x) (q : 0 = y) : x = y => rewriteI p q

\lemma test3 (x y : Nat) (p : 0 = x) (q : 0 = y) : x = y => rewriteF p q

\lemma test4 (x y : Nat) (p : 0 = x) (q : 0 = y) => rewriteF p q

\lemma test5 (x y : Nat) (p : 0 = x) (q : 0 = y) => rewrite p q

\lemma test6 {A : \Set} (x : A) (f : A -> A) (h : \Pi (z : A) -> f z = z) : f (f x) = x
  => rewrite h (rewrite h idp)

\lemma test7 {A : Nat} (x y : A) (f : A -> A) : f (x + y) = f (y + x)
  => rewrite +-comm-rw idp
  
\lemma testOccur {x : Nat} (p : suc x = suc (suc x)) : suc (suc x) = x Nat.+ 3 => rewrite {1} p idp  

\lemma testNorm {A : \Type} (a : A) (l : List A) (P : List A -> \Prop) (p : P (a :: l)) : P ((a :: l) ++ nil)
  => rewrite ++_nil p

\lemma testRestore {A : \Type} (xs ys zs : List A) (P : List A -> List A -> \Prop) (p : P (xs ++ ys) zs) : P (xs ++ ys) (zs ++ nil)
  => rewrite ++_nil p

Algebraic rewrite

Meta rewriteEq allows for more advanced rewriting in algebraic subexpressions. rewriteEq p t : T, where p : a = b, like rewrite replaces literal occurrences of a in T with b, but it also finds and replaces occurrences up to algebraic equivalences. Currently, this meta supports noncommutative monoids and categories.

For example, if ((a * b) * (ide * c)) * (d * ide) is an expression of type Monoid in T, then b * c * ide counts as an occurrence. If p : b * c * ide = x, then rewriteEq p t will rewrite ((a * b) * (ide * c)) * (d * ide) as ((a * x) * d).

Meta rewriteEq also supports specification of numbers of occurrences which works similarly to the one for rewrite. Note that occurrences can overlap in this case. The counting is natural from left to right.

Examples:

\lemma test1 {A : Monoid} (a b c d x : A) (B : A -> \Prop) (p : b * c = x) (t : B (a * x * d)) : B (((a * b) * (ide * c)) * (d * ide))
  => rewriteEq p t
  
\lemma test2 {C : Precat} {a b c d : C} (P : Hom a d -> \Prop) (f : Hom a b) (g : Hom b c) (g' : Hom c b) (h : Hom c d) (p : g ∘ g' = id c) (t : P ((h ∘ g) ∘ (id b ∘ f))) : P ((h ∘ id c ∘ g) ∘ (g' ∘ g ∘ f))
  => rewriteEq p (rewriteEq (idp {_} {(h ∘ g) ∘ (id b ∘ f)}) t)

Extensionality meta

Meta ext proves goals of the form a = {A} a’. It expects (at most) one argument and the type of this argument is called ‘subgoal’. The expected type is called ‘goal’.

• If the goal is f = {\Pi (x_1 : A_1) … (x_n : A_n) -> B} g, then the subgoal is \Pi (x_1 : A_1) … (x_n : A_n) -> f x_1 … x_n = g x_1 … x_n
• If the goal is t = {\Sigma (x_1 : A_1) … (x_n : A_n) (y_1 : B_1 x_1 … x_n) … (y_k : B_k x_1 … x_n) (z_1 : C_1) … (z_m : C_m)} s, where C_i : \Prop and they can depend on x_j and y_l for all i, j, and l, then the subgoal is \Sigma (p_1 : t.1 = s.1) … (p_n : t.n = s.n) D_1 … D_k, where D_j is equal to coe (\lam i => B (p_1 @ i) … (p_n @ i)) t.{k + j - 1} right = s.{k + j - 1}
• If the goal is t = {R} s, where R is a record, then the subgoal is defined in the same way as for \Sigma-types It is also possible to use the following syntax in this case: ext R { | f_1 => e_1 … | f_l => e_l }, which is equivalent to ext (e_1, … e_l)
• If the goal is A = {\Prop} B, then the subgoal is \Sigma (A -> B) (B -> A)
• If the goal is A = {\Type} B, then the subgoal is Equiv {A} {B}
• If the goal is x = {P} y, where P : \Prop, then the argument for ext should be omitted.

simp_coe

Simplifies certain equalities. It expects one argument and the type of this argument is called ‘subgoal’. The expected type is called ‘goal’.

• If the goal is coe (\lam i => \Pi (x : A) -> B x i) f right a = b’, then the subgoal is coe (B a) (f a) right = b.
• If the goal is coe (\lam i => \Pi (x : A) -> B x i) f right = g’, then the subgoal is \Pi (a : A) -> coe (B a) (f a) right = g a.
• If the goal is coe (\lam i => A i -> B i) f right = g’, then the subgoal is \Pi (a : A left) -> coe B (f a) right = g (coe A a right).
• If the type under coe is a higher-order non-dependent function type, simp_coe simplifies it recursively.
• If the goal is (coe (\lam i => \Sigma (x_1 : A_1 i) … (x_n : A_n i) …) t right).n = b’, then the subgoal is coe A_n t.n right = b.
• If the goal is coe (\lam i => \Sigma (x_1 : A_1) … (x_n : A_n) (B_{n+1} i) … (B_k i)) t right = s’, then the subgoal is a \Sigma type consisting of equalities as specified above ignoring fields in \Prop.
• If the type under coe is a record, then simp_coe works similarly to the case of \Sigma types. The copattern matching syntax as in {ext} is also supported.
• All of the above cases also work for goals with {transport} instead of {coe} since the former evaluates to the latter.
• If the goal is transport (\lam x => f x = g x) p q = s, then the subgoal is q *> pmap g p = pmap f p *> s. If f does not depend on x, then the right hand side of the subgoal is simply s.

simplify

Simplifies the expected type.

\func test1 {M : Monoid} (x : M) : x = x * ide
  => simplify

\func test2 {M : Monoid} (x : M) : x * x = (x * (ide * x)) * ide
  => simplify

\func test3 {M : Monoid} (x : M) : ide * x * x * ide = x * ide * x * ide * ide
  => simplify

\func test4 {M : AddMonoid} (x : M) : x + x = x + x + zro
  => simplify

\func test5 {R : Semiring} (x : R) : zro = x * zro
  => simplify

\func test6 {R : Ring} (x : R) : negative (x * x) = x * negative x
  => simplify

\func test6' {R : Ring} (x y : R) : x * negative y = negative (x * y)
  => simplify

\func test7 {R : AddGroup} (x : R) : negative (negative x) = x
  => simplify

\func test8 {R : Ring} (x : R) : x * negative ide = negative x
  => simplify

\func test9 {M : Monoid} (x y : M) (p : x * x = y) : x * (1 * x) = y * 1
  => simplify p