\import Equiv
\import Equiv.Univalence(Equiv-to-=, QEquiv-to-=)
\import Logic
\import Meta
\import Paths

{- |
  `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 => _ (transport, transportInv)

-- | `rewriteI p` is equivalent to `rewrite (inv p)`
\meta rewriteI => _ (transport, transportInv)

{- |
  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 `Paths.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 => _ (Jl, inv, *>, transport, transport_path_pmap, transport_path_pmap-right, transport_path_pmap.conv,
  transport_path_pmap-right.conv, ext, exts)

{- |
  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 there is no subgoal
-}
\meta ext => _ (transport, simp_coe, later, propExt, Equiv, pathOver, prop-isProp, prop-dpi, Equiv-to-=, QEquiv-to-=)

-- | 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 => _ (transport, simp_coe, later, propExt, Equiv, pathOver, prop-isProp, prop-dpi, Equiv-to-=, QEquiv-to-=)