LBool
Require Export internalize_tac Lvw.
Definition bool_enc (b:bool) : term:=
Eval simpl in
if b then .\"t", "f"; "t" else .\"t", "f"; "f".
(*register instance, contains proc-ness of encoding*)
Instance register_bool : registered bool.
Proof.
register bool_enc.
Defined.
Instance bool_enc_inj : inj_reg register_bool.
Proof.
register_inj.
Qed.
Lemma bool_enc_correct (b:bool) (s t:term): proc s -> proc t -> enc b s t >* if b then s else t.
Proof.
destruct b;fcrush.
Qed.
(* For each encoding, LCor must contain tactics that solve goals of form "encode b s t >* match ...end" without generating own subgoals. We use the explicit pattern to avoid unification that unfolds the defined L-term.*)
Hint Extern 0 (app (app (@enc bool _ _) _) _ >* _) => apply bool_enc_correct;value : LCor.
(* register the constructors *)
Instance term_true : internalized true.
Proof.
internalize constructor.
Defined.
Instance term_false : internalized false.
Proof.
internalize constructor.
Defined.
(* boolean neg, and and or*)
Instance term_negb : internalized negb.
Proof.
internalize. destruct y;crush.
Defined.
Instance term_andb : internalized andb.
Proof.
internalize. destruct y; crush.
Defined.
Instance term_orb : internalized orb.
Proof.
internalize. destruct y; crush.
Defined.