# \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.

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 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
```

# 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.