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