Equality

Require Export LBool LNat Encoding Nat SumBool.
Require Import internalize_tac.


Equality of encoded natural numbers


Local Instance term_nat_eqb : internalized eqb.

Proof.

  internalizeR.
abstract (revert y0;induction y;intros [];recStep P; crush).
Defined.


Instance term_nat_eq_dec : internalized nat_eq_dec.

Proof.

  pose (f x y :=to_sumbool (eqb x y)).

  internalizeWith f.
crush.
  apply reflect_dec.

  eapply Nat.eqb_spec.

Defined.


Equality of encoded terms


Local Definition term_eqb :=
  (fix term_eqb s t: bool:=
       match s,t with
    | var n, var m => if decision (n=m) then true else false
    | app s1 t1, app s2 t2 => andb (term_eqb s1 s2) (term_eqb t1 t2)
    | lam s',lam t' => term_eqb s' t'
    | _,_ => false
       end).


Local Instance term_term_eqb : internalized term_eqb.

Proof.

  internalizeR.

  revert y0.
induction y;intros [];recStep P; crush.
  dec;destruct nat_eq_dec;try tauto;crush.

Defined.


Instance term_term_eq_dec : internalized term_eq_dec.

Proof.

  pose (f x y := to_sumbool (term_eqb x y)).

  internalizeWith f.
crush.
  apply reflect_dec.

  revert y0.
induction y as [x | s1 H1 s2 H2| s H];intros [y | t1 t2| t];cbn;try constructor;try congruence.
  -dec;constructor;congruence.

  -specialize (H1 t1).
specialize (H2 t2). do 2 destruct (term_eqb);simpl in *; constructor;inv H1;inv H2;try congruence.
  -destruct (H t);constructor;congruence.

Defined.