From: Enrico Tassi Date: Thu, 16 Oct 2008 16:04:25 +0000 (+0000) Subject: ex for students about induction X-Git-Tag: make_still_working~4679 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c775f53f9aae44897fb13342cd9f2e7ec5e394f7;hp=4ff2055cabd4ac273b7222f6cf21aedbff5c022d;p=helm.git ex for students about induction --- diff --git a/helm/software/matita/contribs/didactic/Makefile b/helm/software/matita/contribs/didactic/Makefile new file mode 100644 index 000000000..a904aaef4 --- /dev/null +++ b/helm/software/matita/contribs/didactic/Makefile @@ -0,0 +1,21 @@ +include ../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)matitac +$(DIR).opt opt all.opt: + $(BIN)matitac.opt +clean: + $(BIN)matitaclean +clean.opt: + $(BIN)matitaclean.opt +depend: + $(BIN)matitadep -dot && rm depends.dot +depend.opt: + $(BIN)matitadep.opt -dot && rm depends.dot +exercise: + rm -rf ex/ + mkdir ex/ + cp *.ma root depends ex/ + for X in ex/*.ma; do perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/.../msg;print' -i $$X; done diff --git a/helm/software/matita/contribs/didactic/depends b/helm/software/matita/contribs/didactic/depends new file mode 100644 index 000000000..6234ee807 --- /dev/null +++ b/helm/software/matita/contribs/didactic/depends @@ -0,0 +1,2 @@ +induction_support.ma +induction.ma induction_support.ma diff --git a/helm/software/matita/contribs/didactic/depends.png b/helm/software/matita/contribs/didactic/depends.png new file mode 100644 index 000000000..3b6104659 Binary files /dev/null and b/helm/software/matita/contribs/didactic/depends.png differ diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma new file mode 100644 index 000000000..4bfe88a8b --- /dev/null +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -0,0 +1,169 @@ +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. + + + diff --git a/helm/software/matita/contribs/didactic/induction_support.ma b/helm/software/matita/contribs/didactic/induction_support.ma new file mode 100644 index 000000000..b8fc7ffc8 --- /dev/null +++ b/helm/software/matita/contribs/didactic/induction_support.ma @@ -0,0 +1,25 @@ +include "nat/minus.ma". + +definition max : nat → nat → nat ≝ + λa,b:nat. + let rec max n m on n ≝ + match n with + [ O ⇒ b + | S n ⇒ + match m with + [ O ⇒ a + | S m ⇒ max n m]] + in + max a b. + +definition min : nat → nat → nat ≝ + λa,b:nat. + let rec min n m on n ≝ + match n with + [ O ⇒ a + | S n ⇒ + match m with + [ O ⇒ b + | S m ⇒ min n m]] + in + min a b. \ No newline at end of file diff --git a/helm/software/matita/contribs/didactic/root b/helm/software/matita/contribs/didactic/root new file mode 100644 index 000000000..8f72072f4 --- /dev/null +++ b/helm/software/matita/contribs/didactic/root @@ -0,0 +1 @@ +baseuri=cic:/matita/didactic