LNat

Require Export internalize_tac.
Require Import SumBool Nat.

Encoding of natural numbers


Fixpoint nat_enc (n : nat) :=
  match n with
  | 0 => lam(lam (# 1))
  | S n => lam(lam (# 0 (nat_enc n)))
  end.


(* do not use this, but (internalizes S) once registered!*)
Definition nat_S : term := Eval simpl in ( .\"n","z","s"; "s" "n").


(*instance contains proc-ness and injectivity of encoding*)
Instance register_nat : registered nat.

Proof.

  register nat_enc.

Defined.


Instance nat_enc_inj : inj_reg register_nat.

Proof.

  register_inj.

Qed.


(* now we must register the constructors*)
Instance term_O : internalized 0.

Proof.

  internalizeC (nat_enc 0).

Defined.


Instance term_S : internalized S.

Proof.

  internalizeC nat_S.

Defined.


(* now the correctnes lemma notice that we must use enc here, not nat_enc!
REPEAT: USE ENC HERE*)

Lemma nat_enc_correct (n:nat) (s t:term): proc s -> proc t -> enc n s t >* match n with 0 => s | S n => t (enc n ) end.

Proof.

  enc_correct.

Qed.


(* the correctnes lemma must be registered in LCor by hand, notice that we use encode here!*)
Hint Extern 0 (app (app (@enc nat _ _) _) _ >* _)=> apply nat_enc_correct;value : LCor.


(* now useful function pred, add and mul *)

Instance term_pred : internalized pred.

Proof.

  internalize.
abstract(destruct y;crush).
Defined.


Instance term_plus : internalized add.

Proof.

  internalizeR.
abstract (induction y; recStep P; crush).
Defined.


Instance term_mult : internalized mult.

Proof.

  internalizeR.
abstract (induction y; recStep P; crush).
Defined.


Instance term_leb : internalized leb.

Proof.

  internalizeR.

  revert y0;induction y;recStep P; crush.
destruct y0;crush.
Defined.


Instance term_nat_le_dec : internalized nat_le_dec.

Proof.

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

  internalizeWith f.
crush.
  apply reflect_dec.

  apply Nat.leb_spec0.

Qed.


(* Notice that we have those two properties as well, just by registering nat_enc:
But for consistency, we do not use them*)

(* Lemma nat_enc_injective : injective nat_enc. *)
(* Proof. *)
(*   exact inj_enc. *)
(* Abort. *)

Lemma nat_enc_proc n : proc (nat_enc n).

Proof.

  exact (proc_enc n).

Abort.


(* now some more encoding-related properties:*)

Fixpoint unenc (s : term) :=
match s with
| lam (lam #1) => Some 0
| lam (lam (app #0 s)) => match unenc s with Some n => Some (S n) | x=>x end
| _ => None
end.


Lemma unenc_correct m : (unenc (nat_enc m)) = Some m.

Proof.

  induction m; simpl; now try rewrite IHm.

Qed.


Lemma unenc_correct2 t n : unenc t = Some n -> nat_enc n = t.

Proof with try now inv H.

  revert n.
eapply (size_induction (f := size) (p := (fun t => forall n, unenc t = Some n -> nat_enc n = t))). clear t. intros t IHt n H.
  destruct t...
destruct t... destruct t...
  -destruct n0...
destruct n0...
  -destruct t1...
destruct n0... simpl in H. destruct (unenc t2) eqn:A.
   +apply IHt in A;simpl;try omega.
destruct n. inv H. simpl. congruence.
   + inv H.

Qed.


Lemma dec_enc t : dec (exists n, t = nat_enc n).

Proof.

  destruct (unenc t) eqn:H.

  - left.
exists n. now eapply unenc_correct2 in H.
  - right.
intros [n A]. rewrite A in H. rewrite unenc_correct in H. inv H.
Qed.