internalize_demo

Require Import LOptions LBool LNat LTactics.
Require Import internalize_tac intermediate Template.Template.

(* Get back terms out of names *)

Goal True.
Proof.
  pose_denote "plus".

  Fail pose_denote "add". (* this does not work at this point *)
  Fail pose_denote "Init.Nat.add". (* this also doesn't work *)
  Require Import Init.Nat.
  pose_denote "add". (* now it works, but only the short forms  *)

  pose_denote "True".
  pose_denote "Coq.Init.Logic.True". (* for types, one can also use the long forms *)
  (* this poses (n := Init.Nat.add : nat -> nat -> nat) to the context *)
  auto.
Qed.

(* for examples of usage see LBool/LNat/Lists/Option/Encoding etc*)

Definition unit_enc := fun (x:unit) => I.

Compute (enc 0, enc false , enc 2).

Goal True.
Proof.
  let x := toTT (eq_dec nat) in
  pose x.
  simpl in t.

Instance register_unit : registered unit.
Proof.
  register unit_enc.
Defined.

(* example for higher-order-stuff *)

Definition on0 (f:nat ->nat ->nat) := f 0 0.

Instance term_on0 : internalized on0.
Proof.
  internalize.
Qed.

Lemma test_Some_nat : internalized (@Some nat ).
Proof.
  internalize.
Qed.

(* this is more or lest just a test for internalization automation... *)
Instance term_option_map X Y (Hy:registered Y) (Hx : registered X) : internalized (@option_map X Y ).
Proof.
  internalize.
  destruct y0; crush.
Qed.

Instance term_nat_eqb : internalized Nat.eqb.
Proof.
  internalizeR. revert y0;induction y;intros [];recStep P; crush.
Defined.

Local Definition testT := fun x : sumbool True False => if x then 2 else 3.

Local Instance test : internalized testT.
Proof.
  internalize. destruct y; crush.
Qed.

(* Definition contains0 A := list_in_dec 0 A. *)
(* Require Import Equality LTactics. *)

(* Goal internalized contains0. *)
(*   internalize. crush. *)
(* Qed.                                      *)