LNat
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.