;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