1 include "induction_support.ma".
3 inductive Formula : Type ≝
5 | FTop: (*BEGIN*)Formula(*END*)
7 | FNot: Formula → Formula
8 | FAnd: (*BEGIN*)Formula → Formula → Formula(*END*)
9 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
10 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
13 let rec sem (v: nat -> nat) (F: formula) on F ≝
16 | FTop ⇒ (*BEGIN*)1(*END*)
18 | FNot F1 ⇒ 1 - sem v F1
19 | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
21 | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
22 | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
27 definition if_then_else ≝
28 λe,t,f.match e return λ_.Formula with [ true ⇒ t | false ⇒ f].
30 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f"
31 non associative with precedence 19
32 for @{ 'if_then_else $e $t $f }.
34 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp"
35 non associative with precedence 19
36 for @{ 'if_then_else $e $t $f }.
38 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t f).
40 let rec subst (x:nat) (G: Formula) (F: formula) on F ≝
43 | FTop ⇒ (*BEGIN*)FTop(*END*)
44 | FAtom n ⇒ if eqb n x then G else (*BEGIN*)(FAtom n)(*END*)
45 | FNot F ⇒ FNot (subst x G F)
47 | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
48 | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
49 | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
53 definition equiv ≝ λv,F1,F2. sem v F1 = sem v F2.
55 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \sub v \nbsp b)"
56 non associative with precedence 45
57 for @{ 'equivF $v $a $b }.
59 notation > "a ≡_ term 90 v b" non associative with precedence 50
60 for @{ equiv $v $a $b }.
62 interpretation "equivalence for Formulas" 'equivF v a b = (equiv v a b).
65 ∀F1,F2,F,x,v. equiv v F1 F2 → equiv v (subst x F1 F) (subst x F2 F).
71 assume H : (F1 ≡_v F2).
72 we proceed by induction on F to prove (subst x F1 F ≡_v subst x F2 F).
74 the thesis becomes (FBot ≡_v (subst x F2 FBot)).
75 the thesis becomes (FBot ≡_v FBot).
76 the thesis becomes (sem v FBot = sem v FBot).
77 the thesis becomes (0 = sem v FBot).
78 the thesis becomes (0 = 0).
82 the thesis becomes (FTop ≡_v FTop).
83 the thesis becomes (sem v FTop = sem v FTop).
84 the thesis becomes (1 = 1).
90 (if eqb n x then F1 else (FAtom n) ≡_v subst x F2 (FAtom n)).
92 (if eqb n x then F1 else (FAtom n) ≡_v
93 if eqb n x then F2 else (FAtom n)).
94 we proceed by cases on (eqb n x) to prove True. (*CSC*)
96 the thesis becomes (F1 ≡_v F2).
99 the thesis becomes (FAtom n ≡_v FAtom n).
100 the thesis becomes (sem v (FAtom n) = sem v (FAtom n)).
101 the thesis becomes (v n = v n).
104 assume (*BEGIN*)f : Formula.(*END*)
105 by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
106 the thesis becomes (FNot (subst x F1 f) ≡_v FNot (subst x F2 f)).
107 the thesis becomes (sem v (FNot (subst x F1 f)) = sem v (FNot (subst x F2 f))).
108 the thesis becomes (1 - sem v (subst x F1 f) = sem v (FNot (subst x F2 f))).
109 the thesis becomes (1 - sem v (subst x F1 f) = 1 - sem v (subst x F2 f)).
110 by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH1).
111 conclude (1-sem v (subst x F1 f)) = (1-sem v (subst x F2 f)) by IH1.
115 by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
117 by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
118 by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
119 by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
121 (sem v (FAnd (subst x F1 f) (subst x F1 f1)) =
122 sem v (FAnd (subst x F2 f) (subst x F2 f1))).
124 (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
125 min (sem v (subst x F2 f)) (sem v (subst x F2 f1))).
127 (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)))
128 = (min (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
129 = (*BEGIN*)(min (sem v (subst x F2 f)) (sem v (subst x F2 f1)))(*END*) by (*BEGIN*)IH3(*END*).
134 by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
136 by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
137 by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
138 by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
140 (sem v (FOr (subst x F1 f) (subst x F1 f1)) =
141 sem v (FOr (subst x F2 f) (subst x F2 f1))).
143 (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
144 max (sem v (subst x F2 f)) (sem v (subst x F2 f1))).
146 (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)))
147 = (max (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
148 = (max (sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3.
152 by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
154 by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
156 (max (1 - sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
157 max (1 - sem v (subst x F2 f)) (sem v (subst x F2 f1))).
158 by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
159 by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
161 (max (1-sem v (subst x F1 f)) (sem v (subst x F1 f1)))
162 = (max (1-sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
163 = (max (1-sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3.