aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Quote.v
blob: 2c373d505200684c32543a9c1531af341403ae0e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
Require Import Quote.

Parameter A B : Prop.

Inductive formula : Type :=
  | f_and : formula -> formula -> formula
  | f_or : formula -> formula -> formula
  | f_not : formula -> formula
  | f_true : formula
  | f_atom : index -> formula
  | f_const : Prop -> formula.

Fixpoint interp_f (vm:
                    varmap Prop) (f:formula) {struct f} : Prop :=
  match f with
  | 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
  | f_const c => c
  end.

Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B).
intro H.
match goal with
  | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H)
end.
match goal with
  |- ?g => quote interp_f [ A ] in g using (fun x => idtac x)
end.
quote interp_f.
Show.
simpl; quote interp_f [ A ].
Show.
Admitted.