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.