(* 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.