{- | `rewrite (p : a = b) t : T` 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` - If the expected type is unknown, the meta rewrites in the type of the arguments instead. - `rewrite {i_1, ... i_k} p t` replaces only occurrences with indices `i_1`, ... `i_k`. Here `i_j` is the number of occurrence after replacing all the previous occurrences. - Also, `p` may be a function, in which case `rewrite p` is equivalent to `rewrite (p _ ... _)`. - `rewrite (p_1, ... p_n) t` is equivalent to `rewrite p_1 (... rewrite p_n t ...)` -} \meta rewrite -- | `rewriteI p` is equivalent to `rewrite (inv p)` \meta rewriteI {- | `rewriteEq (p : a = b) t : T` is similar to {rewrite}, but it finds and replaces occurrences of `a` up to algebraic equivalences. - For example, `rewriteEq (p : b * (c * id) = x) t : T` rewrites `(a * b) * (id * c)` as `a * x` in `T`. - Similarly to `rewrite` this meta allows specification of occurrence numbers. - Currently this meta supports noncommutative monoids and categories. -} \meta rewriteEq -- | Simplifies the expected type or the type of the argument if the expected type is unknown. \meta simplify {- | 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`. - If the expected type is unknown or if the meta is applied to more than one argument, then it applies to the type of the argument instead of the expected type. -} \meta simp_coe {- | 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 -} \meta ext -- | Similar to {ext}, but also applies either {simp_coe} or {ext} when a field of a \Sigma-type or a record has an appropriate type. \meta exts