(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                               DemoQuote.v                                *)
(****************************************************************************)

Require Quote.

Parameters A,B,C:Prop.

(* 1. Without variables map (constants only) *)

Inductive Type formula :=
| f_and : formula -> formula -> formula (* binary constructor *)
| f_or : formula -> formula -> formula  
| f_not : formula -> formula            (* unary *)
| f_true : formula                      (* 0-ary constructor *)
| f_const : Prop -> formula.            (* contructor for constants *)

Fixpoint interp_f [f:formula] : Prop := 
  Cases f of
  | (f_and f1 f2) => (interp_f f1)/\(interp_f f2)
  | (f_or f1 f2) => (interp_f f1)\/(interp_f f2)
  | (f_not f1) => ~(interp_f f1)
  | f_true => True
  | (f_const c) => c
  end.

Goal A/\(A\/True)/\~B/\(A <-> A).
Quote interp_f.
(*******
1 subgoal
  
  ============================
   (interp_f
     (f_and (f_const A)
       (f_and (f_or (f_const A) f_true)
         (f_and (f_not (f_const B)) (f_const A<->A)))))
*********)


(* 2. interpretation function with a variables map *)

Reset formula.

Inductive Set formula :=
| f_and : formula -> formula -> formula
| f_or : formula -> formula -> formula  
| f_not : formula -> formula           
| f_true : formula                     
| f_atom : index -> formula.            (* contructor for variables *)

Fixpoint interp_f [vm:(varmap Prop); f:formula] : Prop := 
  Cases f of
  | (f_and f1 f2) => (interp_f vm f1)/\(interp_f vm f2)
  | (f_or f1 f2) => (interp_f vm f1)\/(interp_f vm f2)
  | (f_not f1) => ~(interp_f vm f1)
  | f_true => True
  | (f_atom i) => (varmap_find True i vm)
  end.

Goal A/\(A\/True)/\~B.
Quote interp_f.
(* in the map 0 |-> B;  1 |-> A the abstract formula is :
    (f_and (f_atom 1) (f_and (f_or (f_atom 1) f_true) (f_not (f_atom O)))) *)
(******
   (interp_f
     (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop))
       (Empty_vm Prop))
     (f_and (f_atom (Left_idx End_idx))
       (f_and (f_or (f_atom (Left_idx End_idx)) f_true)
         (f_not (f_atom End_idx)))))
*******)

(* 3. interpretation function with variables map and constants *)
Reset formula.

Inductive Type formula :=
| f_and : formula -> formula -> formula
| f_or : formula -> formula -> formula
| f_not : formula -> formula
| f_true : formula
| f_const : Prop -> formula             (* contructor for constants *)
| f_atom : index -> formula.            (* contructor for variables *)

Fixpoint interp_f [vm:(varmap Prop); f:formula] : Prop := 
  Cases f of
  | (f_and f1 f2) => (interp_f vm f1)/\(interp_f vm f2)
  | (f_or f1 f2) => (interp_f vm f1)\/(interp_f vm f2)
  | (f_not f1) => ~(interp_f vm f1)
  | f_true => True
  | (f_const c) => c
  | (f_atom i) => (varmap_find True i vm)
  end.

Goal A/\(A\/True)/\~B/\(C<->C).
Quote interp_f.
(********
1 subgoal
  
  ============================
   (interp_f
     (Node_vm C<->C (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
       (Node_vm A (Empty_vm Prop) (Empty_vm Prop)))
     (f_and (f_atom (Right_idx End_idx))
       (f_and (f_or (f_atom (Right_idx End_idx)) f_true)
         (f_and (f_not (f_atom (Left_idx End_idx))) (f_atom End_idx)))))
*********)
Undo. Quote interp_f [A B]. 
(********* Here A and B are constants and the varmap contains only C<->C
1 subgoal
  
  ============================
   (interp_f (Node_vm C<->C (Empty_vm Prop) (Empty_vm Prop))
     (f_and (f_const A)
       (f_and (f_or (f_const A) f_true)
         (f_and (f_not (f_const B)) (f_atom End_idx)))))

************)
Undo. Quote interp_f [B C iff]. 
(******** Here A is in the varmap and B, C <-> C are constants 
 -- understood the difference ?
1 subgoal
  
  ============================
   (interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop))
     (f_and (f_atom End_idx)
       (f_and (f_or (f_atom End_idx) f_true)
         (f_and (f_not (f_const B)) (f_const C<->C)))))
**********)
Abort.

