LBool

Require Export internalize_tac Lvw.

Encoding of booleans


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.