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.