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