(* Use Coq data-structures for programming *)
Require Export List.
Open Scope list_scope.
Inductive form : Set := T | F | Conj : form -> form -> form
| Var : nat -> form.
Definition env := list Prop.
Fixpoint find_env (e:env) (n:nat) {struct e} :=
match e with nil => True
| cons a l => match n with O => a
| S p => find_env l p
end
end.
Fixpoint interp (e:env) (f:form) {struct f} :=
match f with T => True | F => False
| Conj A B => interp e A /\ interp e B
| Var n => find_env e n
end.
Eval compute in
(interp (True::False::(0=0)::nil) (Conj (Var 0) (Conj (Var 2) (Var 1)))).
Ltac env_form l f :=
match f with True => constr:(l,T)
| False => constr:(l,F)
| ?A /\ ? B =>
match env_form l A with
(?l1,?A1) =>
match env_form l1 B with
(?l2,?A2) => constr:(l2,Conj A1 A2) end
end
| ?A => let n := eval compute in (length l)
in constr:(cons A l,Var n)
end.
Ltac reify :=
match goal with |- ?P =>
match (env_form (nil (A:=Prop)) P) with (?l,?f) =>
let e := eval compute in (rev l) in
change (interp e f) end
end.
Lemma test1 : 0=0 /\ (False -> False) /\ 1=1 /\ (0=0).
reify.
Admitted.