Encoding

Require Import internalize_tac LTactics.
Require Export LNat.

Encoding for terms


Fixpoint term_enc (t : term) :=
     match t with
       | var n => lam (lam (lam ((var 2) (enc n))))
       | app s t => lam (lam (lam ((var 1) (term_enc s) (term_enc t))))
       | lam s => lam (lam (lam ((var 0) (term_enc s))))
     end.

Definition Var : term := Eval simpl in .\"n"; .\"v","a","l"; "v" "n".
Definition App : term := Eval simpl in .\"s","t"; .\"v","a","l"; "a" "s" "t".
Definition Lam : term := Eval simpl in .\"s"; .\"v","a","l"; "l" "s".

Instance register_term : registered term.
Proof.
  register term_enc.
Defined.

Instance term_enc_inj : inj_reg register_term.
Proof.
  register_inj.
Qed.

Lemma term_enc_correct (s t u v:term): proc t -> proc u -> proc v ->
                                   enc s t u v >* match s with
                                                       var n => t (enc n)
                                                     | app s1 s2 => u (enc s1) (enc s2)
                                                     | lam s => v (enc s)
                                                   end.
Proof.
  enc_correct.
Qed.

Hint Extern 0 (app (app (app (@enc term _ _) _) _ ) _>* _)=> apply term_enc_correct;value : LCor.

(* register the constructors *)
Instance term_var : internalized var.
Proof.
  internalizeC Var.
Defined.

Instance term_app : internalized app.
Proof.
  internalizeC App.
Defined.

Instance term_lam : internalized lam.
Proof.
  internalizeC Lam.
Defined.

Tactic Notation "test" open_constr(H) := enough H; abstract (exact H).

Interalized encoding of natural numbers

Instance term_nat_enc : internalized (enc (X:=nat)).
Proof.
  internalizeR. abstract (induction y;recStep P; crush).
Defined.

Interalized term encoding

Instance term_term_enc : internalized (enc (X:=term)).
Proof.
  internalizeR. abstract (induction y; recStep P; crush).
Defined.