Library FEqualDep

Require Import ProofIrrelevance.
Require Export FunctionalExtensionality JMeq.
Require Import Common Notations.

Set Implicit Arguments.

Section f_equal_dep.
Theorem f_type_equal {A B A' B'} : A = A'B = B'(AB) = (A'B').
intros; repeat subst; reflexivity.
Qed.

Theorem forall_extensionality_dep : {A}
(f g : AType),
( x, f x = g x) → ( x, f x) = ( x, g x).
intros.
replace f with g; auto.
apply functional_extensionality_dep; auto.
Qed.

Theorem forall_extensionality_dep_JMeq : {A B}
(f : AType) (g : BType),
A = B → (A = B x y, x == yf x == g y) → ( x, f x) = ( x, g x).
intros; firstorder; intuition; repeat subst.
apply forall_extensionality_dep.
intro.
apply JMeq_eq.
eauto.
Qed.

Lemma JMeq_eqT A B (x : A) (y : B) : x == yA = B.
intro H; destruct H; reflexivity.
Qed.

Lemma fg_equal_JMeq A B B' (f : a : A, B a) (g : a : A, B' a) x :
f == g → (f == gB = B') → f x == g x.
intros.
repeat (firstorder; repeat subst).
Qed.

Lemma f_equal_JMeq A A' B B' a b (f : a : A, A' a) (g : b : B, B' b) :
f == g → (f == gA' == B') → (f == ga == b) → f a == g b.
intros.
firstorder.
repeat destruct_type @JMeq.
repeat subst; reflexivity.
Qed.

Lemma f_equal1_JMeq A0 B a0 b0 (f : (a0 : A0), B a0) :
a0 = b0
→ f a0 == f b0.
intros.
repeat (firstorder; repeat subst).
Qed.

Lemma f_equal2_JMeq A0 A1 B a0 b0 a1 b1 (f : (a0 : A0) (a1 : A1 a0), B a0 a1) :
a0 = b0
→ (a0 = b0a1 == b1)
→ f a0 a1 == f b0 b1.
intros.
repeat (firstorder; repeat subst).
Qed.

Lemma f_equal3_JMeq A0 A1 A2 B a0 b0 a1 b1 a2 b2 (f : (a0 : A0) (a1 : A1 a0) (a2 : A2 a0 a1), B a0 a1 a2) :
a0 = b0
→ (a0 = b0a1 == b1)
→ (a0 = b0a1 == b1a2 == b2)
→ f a0 a1 a2 == f b0 b1 b2.
intros.
repeat (firstorder; repeat subst).
Qed.

Lemma f_equal4_JMeq A0 A1 A2 A3 B a0 b0 a1 b1 a2 b2 a3 b3 (f : (a0 : A0) (a1 : A1 a0) (a2 : A2 a0 a1) (a3 : A3 a0 a1 a2), B a0 a1 a2 a3) :
a0 = b0
→ (a0 = b0a1 == b1)
→ (a0 = b0a1 == b1a2 == b2)
→ (a0 = b0a1 == b1a2 == b2a3 == b3)
→ f a0 a1 a2 a3 == f b0 b1 b2 b3.
intros.
repeat (firstorder; repeat subst).
Qed.

Lemma f_equal5_JMeq A0 A1 A2 A3 A4 B a0 b0 a1 b1 a2 b2 a3 b3 a4 b4 (f : (a0 : A0) (a1 : A1 a0) (a2 : A2 a0 a1) (a3 : A3 a0 a1 a2) (a4 : A4 a0 a1 a2 a3), B a0 a1 a2 a3 a4) :
a0 = b0
→ (a0 = b0a1 == b1)
→ (a0 = b0a1 == b1a2 == b2)
→ (a0 = b0a1 == b1a2 == b2a3 == b3)
→ (a0 = b0a1 == b1a2 == b2a3 == b3a4 == b4)
→ f a0 a1 a2 a3 a4 == f b0 b1 b2 b3 b4.
intros.
repeat (firstorder; repeat subst).
Qed.

Lemma eq_JMeq T (A B : T) : A = BA == B.
intro; subst; reflexivity.
Qed.

Theorem functional_extensionality_dep_JMeq : {A} {B1 B2 : AType},
(f : x : A, B1 x) (g : x : A, B2 x),
( x, B1 x = B2 x)
→ ( x, f x == g x) → f == g.
intros.
assert (B1 = B2) by (extensionality x; auto); subst.
assert (f = g) by (extensionality x; apply JMeq_eq; auto).
subst; reflexivity.
Qed.

Theorem functional_extensionality_dep_JMeq' : {A1 A2} {B1 : A1Type} {B2 : A2Type},
(f : x : A1, B1 x) (g : x : A2, B2 x),
A1 = A2
→ (A1 = A2 x y, x == yB1 x = B2 y)
→ (A1 = A2 x y, x == yf x == g y) → f == g.
intros.
intuition; repeat subst.
apply functional_extensionality_dep_JMeq; intros;
intuition.
Qed.
End f_equal_dep.

Inductive identity_dep (A : Type) (a : A) : B : Type, BType :=
identity_dep_refl : identity_dep a a.

Ltac JMeq_eq :=
repeat match goal with
| [ |- _ == _ ] ⇒ apply eq_JMeq
| [ H : _ == _ |- _ ] ⇒ apply JMeq_eq in H
end.

Ltac f_equal_dep_cleanup := JMeq_eq; eta_red.

Ltac f_equal_dep' := intros; f_equal; simpl in *;
match goal with
| [ |- ?f ?a == ?g ?b ] ⇒ apply (@f_equal_JMeq _ _ _ _ a b f g); intros; try reflexivity; repeat subst; intros;
match goal with
| [ |- f == g ] ⇒ f_equal_dep'
| [ |- ?x == ?y ] ⇒ f_equal_dep_cleanup; try reflexivity
| _idtac
end
end; f_equal_dep_cleanup.

Ltac f_equal_dep := intros; f_equal; simpl in *;
repeat match goal with
| [ |- ?f ?a = ?g ?b ] ⇒ apply JMeq_eq; f_equal_dep'
| [ |- ?f ?a == ?g ?b ] ⇒ f_equal_dep'
| _try reflexivity
end; f_equal_dep_cleanup.

Section misc.
Lemma sig_JMeq A0 A1 B0 B1 (a : @sig A0 A1) (b : @sig B0 B1) : A1 == B1proj1_sig a == proj1_sig ba == b.
intros.
destruct_sig.
repeat destruct_type @JMeq.
JMeq_eq; subst.
JMeq_eq.
simpl_eq.
trivial.
Qed.

Lemma proof_irrelevance_JMeq (P Q : Prop) (p : P) (q : Q) (H : P = Q)
: p == q.
subst.
apply eq_JMeq.
apply ProofIrrelevance.proof_irrelevance.
Qed.
End misc.