How do I prove a dependent equality without extra axioms or appealing
to the decidable equality of nat? Furthermore, how do I rewrite the
proof term type and goal simultaneously to work with type checking?
I have a simple, toy problem.
Show that in a dependent type toy appending adds to the dependent part.
This is conceptually simple, but difficult to prove within the language.
Require Import Arith.
Axiom toy : nat -> Prop.
Axiom toy_S : forall n, toy n -> toy (S n).
Definition toy_plus (n i : nat) (w : toy n) : toy (i + n).
induction i; [ apply w | ].
apply (toy_S _ IHi).
Defined.
Theorem toy_regroup (i j n : nat) (le_ji : j <= i) : i - j + (j + n) = i + n.
induction le_ji; [ rewrite Nat.sub_diag; apply eq_refl | ].
rewrite (Nat.sub_succ_l _ _ le_ji).
simpl; rewrite IHle_ji; apply eq_refl.
Qed.
Theorem toy_append (n i j : nat) (le_ji : j <= i) (w : toy n) :
toy_plus n i w = eq_rect _ toy (toy_plus (j+n) (i-j) (toy_plus n j w)) _ (toy_regroup i j n le_ji).
(* ??? *)
Looking for examples, people often use Strecher K / UIP to ignore the proof part.
Since nat has decidable equality, we can use eq_rect_eq_dec, which does work.
Though, it's still not quite trivial.
Require Import Coq.Logic.Eqdep_dec.
Theorem toy_append (n i j : nat) (le_ji : j <= i) (w : toy n) :
toy_plus n i w = eq_rect _ toy (toy_plus (j+n) (i-j) (toy_plus n j w)) _ (toy_regroup i j n le_ji).
generalize (toy_regroup i j n le_ji) as eqin.
induction le_ji.
(* We need to rewrite both the proof and goal simultaneously. *)
rewrite Nat.sub_diag; intros.
(* Thanks to UIP, we don't care exactly which proof was used and can simplify away eq_rect. *)
rewrite <- (eq_rect_eq_dec Nat.eq_dec); apply eq_refl.
(* ... *)
Here, it hides the proof in eq_rect, then leaves it in the goal so it can rewrite both the
proof type and the type using it simultaneously to get the correct type out.
Trying to do it piecewise is ill-typed.
Other libraries I've looked at such as https://ropas.snu.ac.kr/~gil.hur/Heq/doc/src.Heq.html also seem to work this way, using an extra axiom or decidability.
The question:
How do I prove toy_append without extra axioms or appealing
to the decidability of equality in nat? That is, I'm trying
to write a direct proof. Since I am proving it based on the same
structure that the function is using, I think that it should be possible?
Especially, how do I change the type proof term in eq_rect and
simultaneously change the type on the rest of the goal? Once I can
do that, I should be able to proof that, because the proof is the
same, and now that the types are the same, the equality proof is eq_refl,
and the eq_rect can be simplified away.
Trying to use le_ind fails because the le_ji term is used in
the proof part of eq_rect. That can be worked around with
Scheme le_dep_ind := Induction for le Sort Prop.
Theorem toy_append (n i j : nat) (le_ji : j <= i) (w : toy n) :
toy_plus n i w = eq_rect _ toy (toy_plus (j+n) (i-j) (toy_plus n j w)) _ (toy_regroup i j n le_ji).
induction le_ji using le_dep_ind.
(*
The follow tactics fail due to not rewriting the whole term, including the dependent part.
rewrite Nat.sub_diag.
Error: Cannot refine with term
"eq_ind_r
(fun _ : nat =>
toy_plus n j w =
eq_rect (j - j + (j + n)) toy
(toy_plus (j + n) (j - j) (toy_plus n j w))
(j + n) (toy_regroup j j n (le_n j))) ?M1070
(Nat.sub_diag ?M1066)" because a metavariable has several occurrences.
rewrite Nat.sub_diag at 1.
Error: build_signature: no constraint can apply on a dependent argument
*)
But, this still leaves the question of how to simplify both the proof term's type and the rest of the goal simulaneously so it type checks.
Is there a recommended way to represent these types of equalities?
For example, the library mentions using JMeq and eq_dep instead of eq_rect
and has their own approach with existT ... = existT ....
Heterogeneous equalities are sometimes easier with eq_dep than with _ = eq_rect _ _, since you don't need to prove the equality on indices separately and then reason about how that behaves.
Require Import Arith Eqdep.
Axiom toy : nat -> Prop.
Axiom toy_S : forall n, toy n -> toy (S n).
Definition toy_plus (n i : nat) (w : toy n) : toy (i + n).
Proof.
induction i; [ apply w | ].
apply (toy_S _ IHi).
Defined.
Lemma f_eq_dep' (U V : Type) (P : U -> Type) (R : V -> Type) (p q : U) (x : P p)
(y : P q) (g : U -> V) (f : forall p0 : U, P p0 -> R (g p0))
: eq_dep U P p x q y -> eq_dep V R (g p) (f p x) (g q) (f q y).
Proof.
intros []; reflexivity.
Qed.
Theorem toy_append (n i j : nat) (le_ji : j <= i) (w : toy n) :
eq_dep nat toy _ (toy_plus n i w) _ (toy_plus (j+n) (i-j) (toy_plus n j w)).
Proof.
induction le_ji.
- rewrite Nat.sub_diag; cbn. reflexivity.
- rewrite Nat.sub_succ_l by assumption; cbn.
apply f_eq_dep'.
apply IHle_ji.
Qed.
(Edit from asker to summarize comments below)
eq_dep and eq_rect are interchangeable by
Theorem eq_dep_rect (A : Type) (a b : A) (P : A -> Type) (Pa : P a) (Pb : P b) (eqd : eq_dep _ P _ Pa _ Pb) :
{ eq_ab : a = b & Pb = eq_rect a P Pa b eq_ab}.
simple refine (let eq_ab : a = b := _ in _); [ destruct eqd; apply eq_refl | ].
apply (existT _ eq_ab).
destruct eqd; apply eq_refl.
Qed.
Theorem eq_rect_dep (A : Type) (a b : A) (P : A -> Type) (Pa : P a) (Pb : P b) (eq_ab : a = b)
(eqr : Pb = eq_rect a P Pa b eq_ab) : eq_dep A P a Pa b Pb.
destruct eq_ab; rewrite eqr; apply eq_dep_intro.
Qed.
which puts the proof from eq_dep into eq_rect. Depending on whether the proof matches, you could still end up needing UIP to replace the proof.