;Note: (Non-inductive) Solutions to first three problems are easy. ;============================================================= ;;Solution to the problem 1 ;============================================================= ;Prove: (implies (not (in x b)) (= (in x (un a b)) (in x a))) ;Use induction scheme given by (un a b)(Note: (in x a) and (tlp a) also work) ;; Base Case proof obligation (implies (endp a) (implies (not (in x b)) (= (in x (un a b)) (in x a)))) ;;Induction Step proof obligation (implies (and (not (endp a)) (implies (not in x b) (= (in x (un (cdr a) b)) (in x (cdr a))))) (implies (not in x b) (= (in x (un a b)) (in x a)))) ;; Using the following propositional equality ;(p -> (q -> r) = ; (p /\ q -> r)) ;we saw for Proof pattern 1 we will simplify our base case and ;induction step proof obligations: ;;Base Case ;; context ;; BC: (endp a) ;; A1: (not (in x b)) (= (in x (un a b)) (in x a)) ;; <= { def un , def in , BC} (= (in x b) nil) ;; <= {Prop. Deduction} (= (not (not (in x b))) nil) ;;<= {A1} (= (not t) nil) ;;<= {eval} t ;; Induction Step ;; context ;; IS1: (not (endp a)) ;; A1: (not (in x b)) ;; IH (implies (not (in x b)) ;; (= (in x un (cdr a) b) ;; (in x (cdr a))) ;;We can deduce the following: ;; => {A1, Modus Ponens(Prop. Ded)} ;; D1: (= (in x un (cdr a) b) ;; (in x (cdr a))) (= (in x (un a b)) (in x a)) ;;<={def un, IS1} (= (in x (cons (car a) (un (cdr a) b))) (in x a)) ;;<={ def in, IS1} (= (in x (cons (car a) (un (cdr a) b))) (if (= x (car a)) t (in x (cdr a)))) ; Case 1 Extra Context: ; CA1: (= x (car a)) (= (in x (cons (car a) (un (cdr a) b))) (if (= x (car a)) t (in x (cdr a)))) ;;<={def in, 0CA1} (= t t) ; Case 2 Extra Context: ; CA2:(not (= x cara)) (= (in x (cons (car a) (un (cdr a) b))) (if (= x (car a)) t (in x (cdr a)))) ;;<={ def in ,IS1, CA2} (= (in x (un (cdr a) b)) (in x (cdr a))) ;;<={IH} t ;============================================================= ;; Solution for problem number 2 ;============================================================= ;Prove: (= (in x (un a b)) (in x (un b a))) ;;Use Induction scheme given by (un a b) ;;Base case proof obligation (implies (endp a) (= (in x (un a b)) (in x (un b a)))) ;;Induction Step proof obligation (implies (and (not (endp a)) (= (in x (un (cdr a) b)) (in x (un b cdr a)))) (= (in x (un a b)) (in x (un b a)))) ;;Base Case ;; context ;; BC1: (endp a) ;; => {BC1, def in} ;; D1: (not (in x a)) (= (in x (un a b)) (in x (un b a))) ;; <= {Def un, BC1} (= (in x b) (in x (un b a))) ;; <= {D1, instantiate lemma union-other} (= (in x b) (in x b)) ;;Induction step ;;context ;; IS1: (not endp a) ;; IH: (= (in x (un (cdr a) b)) ;; (in x (un b (cdr a)))) (= (in x (un a b)) (in x (un b a))) ;; <= {def un, IS1} (= (in x (cons (car a) (un (cdr a) b))) (in x (un b a))) ;; <= {def in, consp-cons axiom, IS1} (= (if (= x (car a)) t (in x (un (cdr a) b))) (in x (un b a))) ;; <= {IH1} (= (if (= x (car a)) t (in x (un b cdr a))) (in x (un b a))) ;; <={cons axiom: (= a (cons (car a) (cdr a)))} (= (if (= x (car a)) t (in x (un b (cdr a))) (in x (un b (cons (car a) (cdr a))))) ;; Case Analysis: ;; (not (= x (car a))) ;; So the new extended context becomes ;; IS1: (not (endp a)) ;; IH1: (= (in x (un (cdr a) b)) ;; (in x (un b (cdr a)))) ;; CA1: (not (= x (car a))) (= (if ( = x (car a) t (in x (un b (cdr a))) (in x (un b (cons (car a) (cdr a))))) ;; <={CA1,if-false} (= (in x (un b (cdr a))) (in x (un b (cons (car a) (cdr a))))) ;; <= {lemma un-cons-other,CA1,cdr-cons} (= (in x (un b (cdr a))) (in x (un b (cdr a)))) ;; Other Case: ;; (= (x (car a)) ;; So the new extended context becomes ;; IS1: (not (endp a)) ;; IH1: (= (in x (un (cdr a) b)) ;; (in x (un b (cdr a)))) ;; CA2: (= x (car a)) ;; Deduce the following: ;; => { IS1, CA2, def in} ;; D1 : (in x a) (= (if (= x (car a) t (in x un b (cdr a))) (in x un b (cons (car a) (cdr a)))) ;; <= {def in, if-true} (= t (in x (un b a)) ;; <= {lemma Union-def, iff is same as equal in boolean context} (= t (or (in x b) (in x a))) ;; <= {def in, IS1 } (= t (or (in x b) (or (= x (car a)) (in x (cdr a))))) ;; <= {Prop. deduction, CA2} (= t t) ;============================================================= ;; Solution for problem number 3 ;============================================================= (implies (in x a) (in a (un a b))) ;; Base Case (implies (endp a) (implies (in x a) (in x (un a b)))) ;;Using the induction scheme given by (un a b) ;; context ;; BC1: (endp a) ;; A1: (in x a) ;; D1: nil {def in, BC1} (in x (un a b)) ;;<= {Prop. deduction, D1} t ;; Induction step proof obligation (implies (and (not (endp a)) (implies (in x (cdr a)) (in x un (cdr a) b))) (implies (in x a) (in x un a b))) ;; context ;; IS1 (not (endp a)) ;; A1: (in x a) ;; IH1 (implies (in x (cdr a)) ;; (in x (un (cdr a) b)) (implies (in x a) (in x (un a b)) ;;<={def un, IS1} (implies (in x a) (in x (cons (car a) (un (cdr a) b)))) ;;Case Analysis ;;Case 1 (= (x (car a)) ;; Updated Context ;; IS1 (not (endp a)) ;; A1: (in x a) ;; IH1 (implies (in x (cdr a)) ;; (in x (un (cdr a) b)) ;; CA1: (= x (car a)) (in x (cons (car a) (un (cdr a) b)))) ;; <= {def in, consp-cons, car-cons, cdr-cons axiom} (or (= x (car a)) (in x (un (cdr a) b))) ;; <= {Prop. Deduction, CA1} t ;;Case Analysis ;;Case 2 (not (= (x car a))) ;; Updated Context ;; IS1 (not (endp a)) ;; IH (implies (in x (cdr a)) ;; (in x (un (cdr a) b)) ;; A1: (in x a) ;; CA2: (not (= (x (car a)))) ;; D1: (in x (cdr a)) {def in, A1, CA2, Prop. Ded} ;; D3: (in x (un (cdr a) b)) {D1, IH, Modus Ponens} (in x (cons (car a) (un (cdr a) b))) ;; <= {def in*, consp-cons, car-cons, cdr-cons} (or (= x (car a)) (in x (un (cdr a) b))) ;;<= {Prop. Deduction, D3} t ;;NOTE: we could have used the indution scheme of definition of in That would have not required us to ;; do case analysis but in any case we will have to prove PHI in (not (endp a)) /\ (= x (car a)) ;*: I used the other def of in(in second last step), its the same thing. ;============================================================= ;; Solution for problem number 4 ;============================================================= (implies (in x b) (in x (un a b))) ;; context ;; A1: (in x b) (in x (un a b)) ;; <= {lemma union-commutative(Problem 2)} (in x (un b a)) ;; <= {lemma in-union1(Problem 3)} (in x b) ;; <= {A1} t ;============================================================= ;; Solution for problem number 5 ;============================================================= (implies (in x (un*-acc a b)) (in x (un a b))) ;It has a tail-recursive function, so choose its induction scheme, but ;notice that this is not the exact same proof pattern I showed in class. ;In the proofs where you prove (f*-acc x y acc) = (g (f x y) acc), you ;have no choice but to use the IS of f*-acc. But in the following proof ;you could have chosen some other IS and it might still work. ;Proof obligations when IS of (un*-acc a b) is applied: ;; Base Case (implies (endp a) (implies (in x (un*-acc a b)) (in x (un a b))) ;; Context ;; BC1: (endp a) ;; A1: (in x (un*-acc a b)) ;; D1: (in x b) {def un*-acc, BC1} (in x (un a b)) ;; <= {def un, BC1} (in x b) ;; <= {D1} t ;; Induction Step (implies (and (not (endp a)) (implies (in x (un*-acc (cdr a) (cons (car a) b))) (in x (un (cdr a) (cons (car a) b))))) (implies (in x (un*-acc a b)) (in x (un a b))))) ;;Context ;; IS1: (not (endp a)) ;; IH : (implies (in x (un*-acc (cdr a) (cons (car a) b))) ;; (in x (un (cdr a) (cons (car a) b)))) ;; A1: (in x (un*-acc a b)) ;;Deduce the following from reasons on right: ;; D1: (in x (un (cdr a) (cons (car a) b))) {A1, def un*-acc, IH, Modus Ponens} (in x (un a b))) ;; <= {def un, IS1} (in x (cons (car a) (un (cdr a) b)))) ;; Case Analysis ;; Case A (= x (car a)) ;; Extended context ;; CA1: (= x (car a)) (in x (cons (car a) (un (cdr a) b))) ;;<= {def in,IS1,CA1} t ;; Case B ;; Extended context: ;; CA2: (not (= x (car a))) ;; Deduce the following using {} ;; D2: (in x (un (cdr a) b)) {lemma un-cons-other, D1, CA2} (in x (cons (car a) (un (cdr a) b))) ;;<= {def in, IS1, consp-cons, CA2} (in x (un (cdr a) b)) ;; <= {D2} t ;============================================================= ;; Solution for problem number 6 ;============================================================= ;By definition of (fact* n) we get (= (fact*-acc n 1) (fact n)) ;But we cant prove this formula by induction, since the second ;argument is a constant, so we generalize and come up with a lemma, ;to relate fact*-acc and fact. How we came up with this lemma is ;simple: ;Try a few examples ;(fact 3) = 6 ;(fact*-acc 3 1) = 6 ;but (fact*-acc 3 2) = 12 and (fact*-acc 3 5) = 30, ;so (fact*-acc 3 5) = (* 5 (fact 3)) which means: (= (fact*-acc n acc) (* acc (fact n))) ;Remember(Proof Pattern 2) this generalized lemma can only be proven using the ; induction scheme generated by the ; tail-recursive function (fact*-acc n acc) ;; Base Case ;; context ;; BC1: (zp n) (= (fact*-acc n acc) (* acc (fact n))) ;<= {def fact*-acc, fact, BC1} (= acc (* acc 1)) ;<= {arith, assume acc is natp} (= acc acc) ;; Induction Step (implies (and (not (zp n)) (= (fact*-acc (- n 1) (* n acc)) (* (* n acc) fact(- n 1)))) (= (fact*-acc n acc) (* acc (fact n)))) ;; context ;; IS1 (not (zp n)) ;; IH1: (= (fact*-acc (- n 1) (* n acc)) ;; (* (* n acc) fact (- n 1))) (= (fact*-acc n acc) (* acc fact n)))) ;; <= {def fact*-acc , IS1} (= (fact*-acc (- n 1) (* n acc)) (* acc fact n)) ;; <= {IH1} (= (* ( * n acc) fact (- n 1)) (* acc fact n)) ;; <= {assume (natp acc), Arith} (= (* acc (* n fact (- n 1))) (* acc fact n)) ;; <= { IS1 , def fact} (= (* acc (fact n)) (* acc (fact n))) ;============================================================= ;; Solution for problem number 7 ;============================================================= ;scale* opens up(non-recursive def), so we need to prove (= (scale*-acc L n nil) (scale L n)) ;But we cant prove this formula by induction, since the accumulator ;argument is a constant, so we generalize and come up with a lemma, ;to relate scale*-acc and scale. How we came up with this lemma is ;simple: ;Try a few examples ;(scale '(1 2) 3) = (4 5) ;(scale*-acc '(1 2) 3 '(19 21)) = '(21 19 4 5) ;so (scale*-acc '(1 2) 3 '(19 21)) = (app (rev '(19 21)) (scale '(1 2) 3)) ;which means: ;; we will show/prove a more general lemma: (= (scale*-acc L n acc) (app (rev acc) (scale L n))) ;Remember(Proof Pattern 2) this generalized lemma can only be proven using the ; induction scheme generated by the ; accumulator style function (scale*-acc L n acc) ;; Base Case (implies (endp L) (= (scale*-acc L n acc) (app (rev acc) (scale L n)))) ;; context ;; BC1: (endp L) (= (scale*-acc L n acc) (app (rev acc) (scale L n))) ;; <= {def scale*-acc , BC1} (= (rev acc) (app (rev acc) nil)) ;;<= {app-nil lemma} (= (rev acc) (rev acc)) ;; Induction Step ;; Proof obligation(Notice the substitution) (implies (and (not (endp L)) (= (scale*-acc (cdr L) n (cons (+ n (car L) acc))) (app (rev (cons (+ n (car L)) acc)) (scale (cdr L) n)))) (= (scale*-acc L n acc) (app (rev acc) (scale L n)))) ; Context ;; IS1:(not (endp L)) ;; IH: (= (scale*-acc (cdr L) n (cons (+ n (car L) acc))) ;; (app (rev (cons (+ n (car L)) acc)) (scale (cdr L) n))) (=(scale*-acc L n acc) (app (rev acc) (scale L n)))) ;; <= { IS1 , def-scale*-acc , def scale} (= (scale*-acc (cdr L) n (cons n (car L) acc)) (app (app (rev acc) (cons (+ n (car L))(scale (cdr L) n ))))) ;; <= {IH} (= (app (rev (cons (+ n (car L)) acc)) (scale (cdr L) n)) (app (rev acc) (cons (+ n (car L)) (scale (cdr L) n)))) ;;<= {def. rev, conp-cons, car-cdr-cons} (= (app (app (rev acc) (cons (+ n (car L)) nil)) (scale (cdr L) n)) (app (rev acc) (cons (+ n (car L)) (scale (cdr L) n)))) ;<= {app-associative lemma} (= (app (rev acc) (app (cons (+ n (car L)) nil) (scale (cdr L) n))) (app (rev acc) (cons (+ n (car L)) (scale (cdr L) n)))) ;<= {app-cons lemma} (= (app (rev acc) (cons (+ n (car L)) (app nil (scale (cdr L) n)))) (app (rev acc) (cons (+ n (car L)) (scale (cdr L) n)))) ; <= {def app, endp, if-true} (= (app (rev acc) (cons (+ n (car L)) (scale (cdr L) n))) (app (rev acc) (cons (+ n (car L)) (scale (cdr L) n)))) ;============================================================= ;; Solution for problem number 8 ;============================================================= ;8(5pts) What inducton scheme does scale and scale*-acc give rise to? ;Ind Scheme given by (SCALE L n): ;BC: (endp L) => PHI ;IStep: (not (endp L)) /\ PHI|sigma=((L (cdr L))) => PHI ;Ind Scheme given by (SCALE*-acc L n acc): ;BC: (endp L) => PHI ;IStep: (not (endp L)) /\ PHI|sigma=((L (cdr L)) (acc (cons (+ n (car L) acc)))) => PHI ;============================================================= ;; Solution for problem number 9 ;============================================================= ;9(5pts) Apply the induction scheme of scale to (tlp (scale l n)) ;to generate the proof obligations(base case and induction step). ;Base case proof obligation: (implies (endp l) (tlp (scale l n))) ;Ind step proof obligation: (implies (and (not (endp L)) (tlp (scale (cdr l) n))) (tlp (scale l n))) ;Similarily Apply the ;induction scheme of (scale*-acc L n acc) to (= (scale*-acc (app l1 l2) n l3) (app (app (rev l3) (scale l1 n)) (scale l2 n))) ;I cannot apply the induction scheme here(without breaking ;rules of substitution), I will have to generalize this ;formula to apply the Induction scheme. ;============================================================= ;; Bonus points lemma (iff (or (in x A) (in x B)) (in x (un A B))) ;Proof Hint: You can break it into 2 proofs using prop deduction, use ;tautology a <=> b = (a => b) /\ (b => a) ; one direction (implies (or (in x A) (in x B)) (in x (un A B))) We will use the induction scheme indicated by function in (endp a) => phi (not (endp a)) /\ (= x (car a)) => phi (not (endp a)) /\ (= x (car a)) /\ phi( a (cdr a)) To prove phi ;Base Case 1: ; Context ; BC1: (endp a) (=>(or (in x A) (in x B)) (in x (un A B))) ;; <= {def in, def un, BC1} (=> (or t (in x b)) (in x b)) ; <= {prop-deduction, simplification} t ;Base Case2 ;;Context ;; BC2: (not (endp a)) ;; BC3: (= x (car a)) (=>(or (in x A) (in x B)) (in x (un A B))) ;;<= { def in , def un, BC2, BC3} (=> (or t (in x B)) (in x (cons (car a) (un (cdr a) b)))) ;;<= { def in , consp-cons, car-cons, proposition deduction} t ; Induction step ;; Context ;; IS1 : (not (endp a)) ;; IS2 : (not (= x (car a))) ;; IH : (=> (or (in x (cdr a)) ( in x b)) ;; (in x un (cdr a) b)) ;; IS3 : (or (in x a) ( in x b)) ;; we can further deduce from tihs cotext ;;<= { def in,IS1, IS2} ;; D1: (or (in x (cdr a) (in x b)) ;; using D1 we can deduce( unlock) the implication in IH ;; D2: (in x (un (cdr a) b)) (in x (un x a b)) ;;<={def un , IS1} (in x (cons (car a) (un (cdr a) b))) ;;<={def in, IS1, IS2} (in x (un (cdr a) b)) ;;<= D2 t ;;other direction (=> (in x (un A B)) (or (in x A) (in x B))) as before we use the indction scheme generated by in ;;Base Case 1 ;;Context ; BC1: (endp a) (=> (in x (un A B)) (or (in x A) (in x B))) ;;<={ def un, BC1, def in} (=> (in x b) (or nil (in x b))) ;;<={propositional deduction} t ;; Base Case 2 ;; BC2: (not (endp a)) ;; BC3: (= x car a) (=> (in x (un A B)) (or (in x A) (in x B))) ;;<={def in, BC2, BC3, def un} (=> (in x (cons (car a) (un (cdr a) b))) (or t (in x b))) ;;<={ def in, consp-cons, BC3, propositional deduction} t ;;Induction Step ;;Context ;; IS1: (not (endp a)) ;; IS2: (not (= x (car a))) ;; IH (=> (in x (un (cdr a) b )) ;; (or (in x (cdr a)) (in x b))) ;; IS3: (in x (un a b)) ;; <= { IS1, def un} ;; (in x (cons (car a) (un (cdr a) b))) ;; <= { def in, IS2} ;;D1 (in x (un (cdr a) b)) (or (in x A) (in x B)) ;;<={ def in ,IS1, IS2} (or (in x (cdr a)) (in x b)) ;;<= {D1} t