misc

Author: twwar

Learning.lean

@@ -1,3 +1,12 @@
 -- This module serves as the root of the `Learning` library.
 -- Import modules here that should be built as part of the library.
-import Learning.Basic
+-- import Learning.Basic
+-- import Mathlib.Computability
+
+import Learning.Syntax
+import Learning.Lambda
+import Learning.Utils
+import Learning.CombinatoryAlgebra
+import Learning.Implicative.Structure
+
+import Learning.Graph.Utils

Learning/Basic.lean

@@ -1 +1,296 @@
-def hello := "world"
+variable (p q r : Prop)
+set_option linter.unusedVariables false
+
+-- commutativity of ∧ and ∨
+example : p ∧ q ↔ q ∧ p := 
+  Iff.intro
+    (fun (h: p ∧ q) => And.intro h.right h.left)
+    (fun (h: q ∧ p) => And.intro h.right h.left)
+
+-- other properties
+example : (p → (q → r)) ↔ (p ∧ q → r) :=
+  Iff.intro
+    (fun (hpqr : p → q → r) => fun (hpq : p ∧ q) => (hpqr hpq.left) hpq.right )
+    (fun hpqr : p ∧ q → r => fun (hp : p) => fun (hq : q) => hpqr ⟨ hp, hq ⟩ )
+
+example : ¬(p ∧ ¬p) :=
+  fun hpnp : p ∧ ¬p =>
+  show False from hpnp.right hpnp.left
+
+example : (p → q) → (¬q → ¬p) :=
+  fun hpq : p → q =>
+  fun hnq : ¬ q =>
+  fun hp : p =>
+  show False from hnq (hpq hp)
+
+
+section
+
+  open Classical
+
+  example : ¬(p ∧ q) → ¬p ∨ ¬q :=
+    fun hnpq : ¬(p ∧ q) =>
+    byCases
+      (fun hp : p =>
+      byCases
+        (fun hq : q => show ¬p ∨ ¬q from False.elim (hnpq ⟨hp, hq⟩))
+        Or.inr )
+      Or.inl
+
+  example : (((p → q) → p) → p) :=
+    fun hpqp : (p → q) → p =>
+    Or.elim (em p)
+      (id)
+      (fun hnp : ¬p => 
+        have hpq : p → q := fun hp : p => absurd hp hnp
+        show p from hpqp hpq
+      )
+
+end
+
+
+variable (α : Type) (p q : α → Prop)
+
+example : (∃ x : α, r) → r :=
+  fun h : (∃ x : α, r) => Exists.elim h (fun a : α => id)
+
+section
+  open Classical
+
+  example : (x : α) → ∃ y : α, (p y → ∀ z : α, p z) :=
+    fun x : α =>
+    byCases
+      (fun hd : (∀ z : α, p z) => ⟨ x, fun _ => hd ⟩ )
+      (fun hnd : ¬(∀ z : α, p z) =>
+        suffices ey : (∃ y : α, ¬ p y) 
+          from Exists.elim ey
+            (λ y => λ hnpy => ⟨ y, λ hpy => show ∀ z : α, p z from False.elim (hnpy hpy) ⟩ )
+        byContradiction λ hney : ¬(∃ y : α, ¬ p y) => 
+          hnd (λ z : α => byContradiction λ hpz : ¬ p z => hney ⟨ z, hpz ⟩ ) )
+
+end
+
+section 
+
+variable (men : Type) (barber : men)
+variable (shaves : men → men → Prop)
+
+example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False :=
+  have hb : shaves barber barber ↔ ¬ shaves barber barber := h barber
+  suffices np : ¬ shaves barber barber from np (hb.mpr np)
+  fun p : shaves barber barber => (hb.mp p) p
+
+end
+
+def divs (m n : Nat) : Prop := ∃ k : Nat, m*k = n
+
+def irred (n : Nat) : Prop := ∀ m : Nat, divs m n → (m = 1 ∨ m = n)
+
+def prime (n : Nat) : Prop := n > 1 ∧ ∀ (a b : Nat), divs n (a*b) → (divs n a ∨ divs n b)
+
+theorem zero_or_succ (n : Nat) : n = 0 ∨ ∃ l : Nat, n = l.succ :=
+  match n with
+  | Nat.zero => Or.inl rfl
+  | Nat.succ l => Or.inr ⟨ l, rfl ⟩
+
+theorem le_add (n m : Nat) : n ≤ n+m :=
+  match m with
+  | Nat.zero => calc
+    n ≤ n := Nat.le_refl n
+    n = n + Nat.zero := rfl
+  | Nat.succ l => calc
+    n ≤ n+l := le_add n l
+    n+l ≤ (n+l).succ := Nat.le_succ (n+l)
+    (n+l).succ = n+l.succ := Eq.symm (Nat.add_succ n l)
+
+theorem le_mul (n k : Nat) : (0 < k) → n ≤ n*k :=
+  λ hk : 0<k => match k with
+  | 0 => absurd hk (Nat.not_lt_zero 0)
+  | Nat.succ l => calc
+    n <= n + (n*l) := le_add n (n*l)
+    n + (n*l) = n*1 + n*l := by simp
+    n*1 + n*l = n*(l+1) := by rw [Nat.add_comm l 1, Nat.mul_add n 1 l]
+    
+theorem nats_integral (n m : Nat) : 0 < n*m → 0 < n :=
+  match n with
+  | 0 => 
+    λ hnm : 0 < 0*m =>
+    have con : 0 < 0 := calc
+      0 < 0*m := hnm
+      0*m = 0 := by simp
+    absurd con (Nat.lt_irrefl 0)
+  | Nat.succ l => (λ hnm : 0 < (l.succ)*m => Nat.zero_lt_succ l)
+
+theorem divs_zero (n : Nat) : divs 0 n → 0=n :=
+  λ ⟨k, h0kn⟩ => calc
+    0 = 0*k := by simp
+    0*k = n := h0kn
+
+theorem divs_le (m n : Nat) : n>0 → divs m n → m ≤ n :=
+  λ hn => 
+  λ ⟨k, hmkn⟩ => 
+  have hkm : 0 < k*m := calc 
+    0 < n := hn
+    n = m*k := Eq.symm hmkn
+    m*k = k*m := Nat.mul_comm m k
+  calc
+    m <= m*k := le_mul m k (nats_integral k m hkm)
+    m*k = n := hmkn
+
+theorem le_irre (m n : Nat) (hmn : m ≤ n) (hnm : n ≤ m) : m=n :=
+  have hor : m=n ∨ m < n := Nat.eq_or_lt_of_le hmn
+  Or.elim hor
+    (id)
+    (λ mltn =>
+      have nltn : n < n := calc
+        n ≤ m := hnm
+        m < n := mltn
+      absurd nltn (Nat.lt_irrefl n))
+
+theorem antisymm_divs (m n : Nat) : divs m n ∧ divs n m → m = n :=
+  λ ⟨ hmn, hnm ⟩ =>
+  match m with
+  | 0 => divs_zero n hmn
+  | Nat.succ m₁ =>
+    let ⟨k, (hk : n*k = m₁+1)⟩ := hnm
+    have npos: n>0 := nats_integral n k (calc 
+      0 < m₁+1 := Nat.succ_pos m₁
+      m₁+1 = n*k := Eq.symm hk)
+    have mlen : m₁+1 ≤ n := divs_le (m₁+1) n npos hmn
+    have nlem : n ≤ m₁+1 := divs_le n (m₁+1) (Nat.succ_pos m₁) hnm
+    (le_irre (m₁+1) n mlen nlem)
+    
+theorem one_divs (n : Nat) : divs 1 n := ⟨ n, Nat.one_mul n ⟩
+
+theorem right_cancel_mul (m n k : Nat) (npos : n>0) (h : m*n = k*n) : m=k :=
+  have tric := Nat.lt_trichotomy m k
+  by
+    apply Or.elim tric
+    . intro mltk
+      have mnltkn := (@Nat.mul_lt_mul_right n m k npos).mpr mltk
+      rw [←h] at mnltkn
+      exact False.elim ((Nat.lt_irrefl (m*n)) mnltkn)
+    . intro dic
+      apply Or.elim dic
+      . exact id
+      . intro kltm
+        have knltmn := (@Nat.mul_lt_mul_right n k m npos).mpr kltm
+        rw [←h] at knltmn
+        exact False.elim ((Nat.lt_irrefl (m*n)) knltmn)
+
+
+theorem primes_are_irred (n : Nat) : prime n → irred n :=
+  λ hn : prime n => 
+  -- have ng1 : n > 1 := hn.left
+  have npos : 0 < n := calc
+    0 < 1 := Nat.zero_lt_succ 0
+    1 < n := hn.left
+  λ m : Nat =>
+  λ ⟨ k, hk ⟩ =>
+  have hndiv : divs n (m*k) := ⟨ 1, Eq.trans (Nat.mul_one n) (Eq.symm hk) ⟩
+  have hdivor : divs n m ∨ divs n k := hn.right m k hndiv
+  Or.elim hdivor
+    (λ ndivm => (Or.inr (antisymm_divs m n ⟨ ⟨k, hk ⟩, ndivm ⟩)) )
+    (λ ⟨ j, (hj : n*j=k) ⟩ => 
+      have h : 1*n = m*j*n := calc
+        1*n = n := Nat.one_mul n
+        n = m*(n*j) := by rw [hj, hk]
+        m*(n*j) = m*j*n := by rw [Nat.mul_comm n j, Nat.mul_assoc m j n]
+      have mj1 : m*j=1 := right_cancel_mul (m*j) n 1 npos (Eq.symm h)
+      have mdiv1 : divs m 1 := ⟨ j ,mj1 ⟩ 
+      show m=1 ∨ m=n from Or.inl (antisymm_divs m 1 ⟨ mdiv1, one_divs m ⟩ ))
+
+section 
+variable (p q r s : Prop)
+
+example : s ∧ q ∧ r → p ∧ r → q ∧ p := by
+  intro ⟨_, ⟨hq, _⟩⟩ ⟨hp, _⟩
+  exact ⟨hq, hp⟩
+end
+
+
+example :
+    (fun (x : Nat × Nat) (y : Nat × Nat) => x.1 + y.2)
+    =
+    (fun (x : Nat × Nat) (z : Nat × Nat) => z.2 + x.1) := by
+  funext (a, b) (c, d)
+  show a + d = d + a
+  rw [Nat.add_comm]
+
+
+namespace Hidden
+
+universe u
+
+theorem symm {α : Type u} {a b : α} (h : Eq a b) : Eq b a :=
+  match h with
+  | rfl => rfl
+
+theorem trans {α : Type u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=
+  match h₁, h₂ with
+  | rfl, rfl => rfl
+
+theorem congr {α β : Type u} {a b : α} (f : α → β) (h : Eq a b) : Eq (f a) (f b) :=
+  match h with
+  | rfl => rfl
+end Hidden
+
+
+inductive Expr where
+  | const : (n : Nat) → Expr
+  | var : (n : Nat) → Expr
+  | plus : (s : Expr) → (t : Expr) → Expr
+  | times : (s : Expr) → (t : Expr) → Expr
+deriving Repr
+
+def Valuation := (Nat → Nat)
+
+def eval_expr (s : Expr) (ρ : Valuation) : Nat :=
+  match s with
+  | Expr.const n => n
+  | Expr.var n => ρ n
+  | Expr.plus s t => (eval_expr s ρ) + (eval_expr t ρ)
+  | Expr.times s t => (eval_expr s ρ) * (eval_expr t ρ)
+
+-- #eval eval_expr (Expr.plus (Expr.var 3) (Expr.times (Expr.const 2) (Expr.var 5))) (1+.)
+
+theorem eval_plus_comm (s t : Expr) (ρ : Valuation) : eval_expr (Expr.plus s t) ρ = eval_expr (Expr.plus t s) ρ :=
+  have lhs : eval_expr (Expr.plus s t) ρ = (eval_expr s ρ) + (eval_expr t ρ) := rfl
+  have rhs : eval_expr (Expr.plus t s) ρ = (eval_expr t ρ) + (eval_expr s ρ) := rfl
+  by rewrite [lhs, rhs]; apply Nat.add_comm
+
+def sampleVal : Nat → Nat
+  | 0 => 5
+  | 1 => 6
+  | _ => 0
+
+def sampleExpr : Expr :=
+  Expr.plus (Expr.times (Expr.var 0) (Expr.const 7)) (Expr.times (Expr.const 2) (Expr.var 1))
+
+#eval eval_expr sampleExpr sampleVal
+
+open Expr
+
+def simpConst : Expr → Expr
+  | plus (const n₁) (const n₂)  => const (n₁ + n₂)
+  | times (const n₁) (const n₂) => const (n₁ * n₂)
+  | e                           => e
+
+def fuse : Expr → Expr
+  | plus s t => simpConst ( plus (simpConst s) (simpConst t))
+  | times s t => simpConst ( times (simpConst s) (simpConst t))
+  | e => e
+
+#eval fuse (plus (const 2) (plus (const 2) (const 3)))
+
+theorem simpConst_eq (v : Valuation)
+        : ∀ e : Expr, eval_expr (simpConst e) v = eval_expr e v := by
+  intros e
+  unfold simpConst
+  split <;> repeat first | rfl | unfold eval_expr
+
+theorem fuse_eq (v : Nat → Nat)
+        : ∀ e : Expr, eval_expr (fuse e) v = eval_expr e v := by
+  intros e
+  unfold fuse
+  split <;> repeat first | rfl | rw [simpConst_eq] | rw [eval_expr]

Learning/CombinatoryAlgebra.lean

@@ -0,0 +1,18 @@
+import Mathlib.Data.Set.Defs
+
+class ApplicativeStructure (α : Type _) where
+  app : α → α → α
+
+class KComb (α : Type _) where
+  K : α
+
+class SComb (α : Type _) where
+  S : α
+
+class CombinatoryAlgebra (α : Type _)
+  extends ApplicativeStructure α, KComb α, SComb α where
+  KComb_def : ∀ x y : α, app (app K x) y = x
+  SComb_def : ∀ x y z : α, app (app (app S x) y) z = app (app x z) (app y z)
+
+def KleeneImp {α : Type _} [hα : ApplicativeStructure α] : Set α → Set α → Set α :=
+  λ A B => {x : α | ∀ a ∈ A, hα.app x a ∈ B}