# Library Equality

Require Export Encoding.

# Equality of encoded natural numbers

Definition EqN := R (.\"EqN", "n", "m"; "n" ("m" true false_1) (.\"n"; "m" false (.\"m"; "EqN" "n" "m"))).

Lemma EqN_rec_00 : EqN (enc 0) (enc 0) == true.

Proof.

crush.

Qed.

Lemma EqN_rec_0S n : EqN (enc 0) (enc (S n)) == false.

Proof.

crush.

Qed.

Lemma EqN_rec_S0 n : EqN (enc (S n)) (enc 0) == false.

Proof.

crush.

Qed.

Lemma EqN_rec_SS n m : EqN (enc (S n)) (enc (S m)) == EqN (enc n) (enc m) .

Proof.

crush.

Qed.

Lemma EqN_correct m n : m = n /\ EqN (enc m) (enc n) == true \/ m <> n /\ EqN (enc m) (enc n) == false.

Proof with eauto.

revert n; induction m; intros.

- destruct n.

+ eauto using EqN_rec_00.

+ eauto using EqN_rec_0S.

- destruct n.

+ eauto using EqN_rec_S0.

+ destruct (IHm n) as [[? ?] | [? ?]].

* left; split...
now rewrite EqN_rec_SS.
* right; split...
now rewrite EqN_rec_SS.
Qed.

# Equality of encoded terms

Definition Eq := R (.\ "Eq", "s", "t"; "s" (.\"n"; "t" (.\"m"; !EqN "m" "n") false_2 false_1)
(.\"s1", "s2"; "t" false_1 (.\"t1","t2"; !Andalso ("Eq" "s1" "t1") ("Eq" "s2" "t2")) false_1)
(.\"s1"; "t" false_1 false_2 (.\"t1"; "Eq" "s1" "t1")) ).

Hint Unfold Eq : cbv.

Lemma Eq_correct_t s t :
(s = t -> Eq (tenc s) (tenc t) == true ).

Proof with try crush.

intros [].

induction s.

+ transitivity (EqN (enc n) (enc n)).

crush.
destruct ( EqN_correct n n) as [E | H]; tauto.
+ transitivity (Andalso !((lam (Eq #0)) (tenc s1) (tenc s1)) !((lam (Eq #0)) (tenc s2) (tenc s2))).

crush.
cbv; now rewrite !Eta, IHs1, IHs2, Andalso_rec_tt; value.
+ transitivity (((lam (Eq #0)) (tenc s)) (tenc s)).

crush.
cbv; now rewrite Eta; value.
Qed.

Lemma Eq_correct_f s t :
( s <> t -> Eq (tenc s) (tenc t) == false ).

Proof with eauto using Andalso_rec_ft, Andalso_rec_tf; try now crush.

revert t; induction s; intros t H.

+ destruct t; [ | now crush | now crush].

transitivity ((EqN (enc n0) (enc n))).
crush.
destruct (EqN_correct n0 n) as [[? ?] | ?]; intuition.
exfalso; intuition.
+ destruct t; [ crush | idtac | crush ..].

* transitivity (Andalso !((lam (Eq #0)) (tenc s1) (tenc t1)) !((lam (Eq #0)) (tenc s2) (tenc t2))).
crush.
destruct (term_eq_dec s1 t1) as [A|A]; destruct (term_eq_dec s2 t2) as [B|B]; cbv; rewrite !Eta; value.

- exfalso.
subst. tauto.
- rewrite IHs2.
apply Eq_correct_t in A. rewrite A... eassumption.
- rewrite IHs1, Eq_correct_t...

- rewrite IHs1, IHs2...

+ destruct t; [ crush .. | ].

* transitivity ((Eq (tenc s) (tenc t))).
crush.
eapply IHs.
congruence.
Qed.

Lemma Eq_correct s t :
(s = t -> Eq (tenc s) (tenc t) == true )
/\ ( s <> t -> Eq (tenc s) (tenc t) == false ).

Proof.

split.
eapply Eq_correct_t. eapply Eq_correct_f.
Qed.