--- /dev/null
+include "induction_support.ma".
+
+inductive Formula : Type ≝
+| FBot: Formula
+| FTop: (*BEGIN*)Formula(*END*)
+| FAtom: nat → Formula
+| FNot: Formula → Formula
+| FAnd: (*BEGIN*)Formula → Formula → Formula(*END*)
+| FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
+| FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
+.
+
+let rec sem (v: nat -> nat) (F: formula) on F ≝
+ match F with
+ [ FBot ⇒ 0
+ | FTop ⇒ (*BEGIN*)1(*END*)
+ | FAtom n ⇒ v n
+ | FNot F1 ⇒ 1 - sem v F1
+ | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
+ (*BEGIN*)
+ | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
+ | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
+ (*END*)
+ ]
+.
+
+definition if_then_else ≝
+ λe,t,f.match e return λ_.Formula with [ true ⇒ t | false ⇒ f].
+
+notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f"
+non associative with precedence 19
+for @{ 'if_then_else $e $t $f }.
+
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp"
+non associative with precedence 19
+for @{ 'if_then_else $e $t $f }.
+
+interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t f).
+
+let rec subst (x:nat) (G: Formula) (F: formula) on F ≝
+ match F with
+ [ FBot ⇒ FBot
+ | FTop ⇒ (*BEGIN*)FTop(*END*)
+ | FAtom n ⇒ if eqb n x then G else (*BEGIN*)(FAtom n)(*END*)
+ | FNot F ⇒ FNot (subst x G F)
+ (*BEGIN*)
+ | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
+ | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
+ | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
+ (*END*)
+ ].
+
+definition equiv ≝ λv,F1,F2. sem v F1 = sem v F2.
+
+notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \sub v \nbsp b)"
+non associative with precedence 45
+for @{ 'equivF $v $a $b }.
+
+notation > "a ≡_ term 90 v b" non associative with precedence 50
+for @{ equiv $v $a $b }.
+
+interpretation "equivalence for Formulas" 'equivF v a b = (equiv v a b).
+
+theorem substitution:
+ ∀F1,F2,F,x,v. equiv v F1 F2 → equiv v (subst x F1 F) (subst x F2 F).
+assume F1 : Formula.
+assume F2 : Formula.
+assume F : Formula.
+assume x : ℕ.
+assume v : (ℕ → ℕ).
+assume H : (F1 ≡_v F2).
+we proceed by induction on F to prove (subst x F1 F ≡_v subst x F2 F).
+case Bot.
+ the thesis becomes (FBot ≡_v (subst x F2 FBot)).
+ the thesis becomes (FBot ≡_v FBot).
+ the thesis becomes (sem v FBot = sem v FBot).
+ the thesis becomes (0 = sem v FBot).
+ the thesis becomes (0 = 0).
+ done.
+case Top.
+ (*BEGIN*)
+ the thesis becomes (FTop ≡_v FTop).
+ the thesis becomes (sem v FTop = sem v FTop).
+ the thesis becomes (1 = 1).
+ (*END*)
+ done.
+case Atom.
+ assume n : ℕ.
+ the thesis becomes
+ (if eqb n x then F1 else (FAtom n) ≡_v subst x F2 (FAtom n)).
+ the thesis becomes
+ (if eqb n x then F1 else (FAtom n) ≡_v
+ if eqb n x then F2 else (FAtom n)).
+ we proceed by cases on (eqb n x) to prove True. (*CSC*)
+ case True.
+ the thesis becomes (F1 ≡_v F2).
+ done.
+ case False.
+ the thesis becomes (FAtom n ≡_v FAtom n).
+ the thesis becomes (sem v (FAtom n) = sem v (FAtom n)).
+ the thesis becomes (v n = v n).
+ done.
+case Not.
+ assume (*BEGIN*)f : Formula.(*END*)
+ by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
+ the thesis becomes (FNot (subst x F1 f) ≡_v FNot (subst x F2 f)).
+ the thesis becomes (sem v (FNot (subst x F1 f)) = sem v (FNot (subst x F2 f))).
+ the thesis becomes (1 - sem v (subst x F1 f) = sem v (FNot (subst x F2 f))).
+ the thesis becomes (1 - sem v (subst x F1 f) = 1 - sem v (subst x F2 f)).
+ by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH1).
+ conclude (1-sem v (subst x F1 f)) = (1-sem v (subst x F2 f)) by IH1.
+ done.
+case And.
+ assume f : Formula.
+ by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
+ assume f1 : Formula.
+ by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
+ by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
+ by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
+ the thesis becomes
+ (sem v (FAnd (subst x F1 f) (subst x F1 f1)) =
+ sem v (FAnd (subst x F2 f) (subst x F2 f1))).
+ the thesis becomes
+ (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
+ min (sem v (subst x F2 f)) (sem v (subst x F2 f1))).
+ conclude
+ (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)))
+ = (min (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
+ = (*BEGIN*)(min (sem v (subst x F2 f)) (sem v (subst x F2 f1)))(*END*) by (*BEGIN*)IH3(*END*).
+ done.
+(*BEGIN*)
+case Or.
+ assume f : Formula.
+ by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
+ assume f1 : Formula.
+ by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
+ by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
+ by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
+ the thesis becomes
+ (sem v (FOr (subst x F1 f) (subst x F1 f1)) =
+ sem v (FOr (subst x F2 f) (subst x F2 f1))).
+ the thesis becomes
+ (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
+ max (sem v (subst x F2 f)) (sem v (subst x F2 f1))).
+ conclude
+ (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)))
+ = (max (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
+ = (max (sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3.
+ done.
+case Implication.
+ assume f : Formula.
+ by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
+ assume f1 : Formula.
+ by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
+ the thesis becomes
+ (max (1 - sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
+ max (1 - sem v (subst x F2 f)) (sem v (subst x F2 f1))).
+ by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
+ by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
+ conclude
+ (max (1-sem v (subst x F1 f)) (sem v (subst x F1 f1)))
+ = (max (1-sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
+ = (max (1-sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3.
+ done.
+(*END*)
+qed.
+
+
+
projects / helm.git / commitdiff
