intial

.vscode/extensions.json

@@ -0,0 +1,13 @@
+{
+	// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
+	// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
+
+	// List of extensions which should be recommended for users of this workspace.
+	"recommendations": [
+
+	],
+	// List of extensions recommended by VS Code that should not be recommended for users of this workspace.
+	"unwantedRecommendations": [
+
+	]
+}

src/instructor/lectures/lecture_22.lean

@@ -105,7 +105,7 @@ begin
   rw int.distrib_right _ _ _,     -- LIBRARY LOOKUP!
   rw <-h2pf,
   rw <-h1pf,
-  ring,
+  ring, -- the rest is true by simple algebra 
 end
 
 /-

src/instructor/lectures/lecture_29a.lean

@@ -233,7 +233,7 @@ begin
   -- that follow "usual" rules of arithmetic
   ring,    
 end
-
+--take away the patterns! look for a way to turn your goal into a statement that can be rewritten to solve with your induction hypothesis 
 
 
 

src/instructor/lectures/lecture_8.lean

@@ -1,4 +1,26 @@
+theorem and_associate : 
+  ∀ (P Q R : Prop), (P ∧ Q) ∧ R → P ∧ (Q ∧ R) :=
+
+begin 
+  assume P Q R,
+  assume h, 
+  have pq : P ∧ Q := and.elim_left h, 
+  have p : P := and.elim_left pq, 
+  have q : Q := and.elim_right pq, 
+  have r : R := and.elim_right h, 
+  exact and.intro p (and.intro q r),
+end
+
+
+
 /-
+<<<<<<< HEAD
+apply can have placeholders which become sub goals of the proof
+you can replace exact with reply but not always the other way around 
+
+top down structured proofs / programing  
+
+=======
 -/
 
 theorem and_associative : 
@@ -14,6 +36,7 @@ begin
 end
 
 /-
+>>>>>>> 12a00a0280a66121314f050808b162610d864adc
 The or connective, ∨, in predicate logic
 join any two propositions, P, Q, into a
 larger proposition, P ∨ Q. This proposition
@@ -77,8 +100,9 @@ axioms (Joe_is_tall Joe_chews_gum : Prop)
 axiom jcg: Joe_chews_gum
 
 theorem jcg_or_jit: Joe_chews_gum ∨ Joe_is_tall :=
-  or.intro_left Joe_is_tall jcg 
-
+  begin 
+    apply or.intro_left Joe_is_tall jcg, 
+  end 
 /-
 We thus have two inference rules (axioms) that we
 can use to create a proof of a "disjunction". 

src/mywork/10-29.lean

@@ -0,0 +1,16 @@
+def cong_mod (n a b : ℤ) : Prop :=
+  ∃ k, a - b = k * n
+
+#reduce cong_mod (4:ℤ)
+#reduce cong_mod (4:ℤ) (6:ℤ) (10:ℤ) --evaluates to the proposition
+
+
+example : cong_mod (4:ℤ) (6:ℤ) (14:ℤ) :=
+begin
+  unfold cong_mod,
+  apply exists.intro (-2:ℤ) _,
+  apply eq.refl,
+end
+
+--in functional programming, if we have a function that takes three arguments we can consider it a function that takes in one number and returns a function with two inputs and so on
+-- this means we are partially evaluating the function by giving it the single number 4. 

src/mywork/hw will be uploaded soon.lean

@@ -0,0 +1,44 @@
+example: 0 ≠ 1 :=
+begin
+  assume a, --intro rule for negation. This means ¬ (0=1) or (0=1) → false
+  cases a, --for all possible proofs of 0 = 1 it is empty and therefore implies false
+end
+
+example : 0 ≠ 0 → 2 = 3 :=
+begin
+  assume a,
+  apply false.elim; -- does false.elim know that 2 ≠ 3? 
+  apply a (eq.refl 0), -- you can also use the contradiction tactic. Looks for a proof of false or p and not p
+end 
+
+example : ∀ (P : Prop), P → ¬ ¬ P :=
+begin
+  assume p b c, --not not p is not p implies false then (p implies false) implies false
+  --have a : p ∧ ¬p := and.intro b c, -- contradiction
+  --have f := c b, or do this and apply f.
+  contradiction, -- there could also be case analysis to show no proofs of false
+end  
+
+axioms em : ∀ (p : Prop), p ∨ ¬p
+
+
+theorem neg_elim : ∀ (P : Prop), ¬¬P → P :=
+begin
+  assume p,
+  assume h,
+  have ponp := classical.em p,
+  cases ponp with p pn,
+  assumption, -- proof is in my list of assumptions
+  contradiction,
+  -- we have nothing to apply our function h to
+  -- we have nothing to work with
+
+end -- this works in classical reasoning but this is not valid in leand constructive logic
+-- given the current axioms we can not prove this, we need to define this as an axiom. We can have it and we can not have this as an axiom
+
+-- axioms em : ∀ (p : Prop), p ∨ ¬p only use this if you want classical reasoning 
+--the hw will need this exclusion of the middle axiom
+-- using case analysis comes from a disjunction
+
+
+-- everything on hw is proovable