From 6ce6b1270712919052c665801bce379522089ed6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 May 2022 19:21:30 -0700 Subject: [PATCH] doc: NFM'22 examples --- doc/examples/NFM2022/nfm1.lean | 20 ++++++++++++ doc/examples/NFM2022/nfm10.lean | 0 doc/examples/NFM2022/nfm11.lean | 0 doc/examples/NFM2022/nfm12.lean | 27 ++++++++++++++++ doc/examples/NFM2022/nfm13.lean | 20 ++++++++++++ doc/examples/NFM2022/nfm14.lean | 13 ++++++++ doc/examples/NFM2022/nfm15.lean | 17 ++++++++++ doc/examples/NFM2022/nfm16.lean | 0 doc/examples/NFM2022/nfm17.lean | 17 ++++++++++ doc/examples/NFM2022/nfm18.lean | 0 doc/examples/NFM2022/nfm19.lean | 8 +++++ doc/examples/NFM2022/nfm2.lean | 12 +++++++ doc/examples/NFM2022/nfm20.lean | 0 doc/examples/NFM2022/nfm21.lean | 0 doc/examples/NFM2022/nfm22.lean | 0 doc/examples/NFM2022/nfm23.lean | 0 doc/examples/NFM2022/nfm24.lean | 9 ++++++ doc/examples/NFM2022/nfm3.lean | 55 +++++++++++++++++++++++++++++++++ doc/examples/NFM2022/nfm4.lean | 0 doc/examples/NFM2022/nfm5.lean | 19 ++++++++++++ doc/examples/NFM2022/nfm6.lean | 0 doc/examples/NFM2022/nfm7.lean | 23 ++++++++++++++ doc/examples/NFM2022/nfm8.lean | 17 ++++++++++ doc/examples/NFM2022/nfm9.lean | 39 +++++++++++++++++++++++ 24 files changed, 296 insertions(+) create mode 100644 doc/examples/NFM2022/nfm1.lean create mode 100644 doc/examples/NFM2022/nfm10.lean create mode 100644 doc/examples/NFM2022/nfm11.lean create mode 100644 doc/examples/NFM2022/nfm12.lean create mode 100644 doc/examples/NFM2022/nfm13.lean create mode 100644 doc/examples/NFM2022/nfm14.lean create mode 100644 doc/examples/NFM2022/nfm15.lean create mode 100644 doc/examples/NFM2022/nfm16.lean create mode 100644 doc/examples/NFM2022/nfm17.lean create mode 100644 doc/examples/NFM2022/nfm18.lean create mode 100644 doc/examples/NFM2022/nfm19.lean create mode 100644 doc/examples/NFM2022/nfm2.lean create mode 100644 doc/examples/NFM2022/nfm20.lean create mode 100644 doc/examples/NFM2022/nfm21.lean create mode 100644 doc/examples/NFM2022/nfm22.lean create mode 100644 doc/examples/NFM2022/nfm23.lean create mode 100644 doc/examples/NFM2022/nfm24.lean create mode 100644 doc/examples/NFM2022/nfm3.lean create mode 100644 doc/examples/NFM2022/nfm4.lean create mode 100644 doc/examples/NFM2022/nfm5.lean create mode 100644 doc/examples/NFM2022/nfm6.lean create mode 100644 doc/examples/NFM2022/nfm7.lean create mode 100644 doc/examples/NFM2022/nfm8.lean create mode 100644 doc/examples/NFM2022/nfm9.lean diff --git a/doc/examples/NFM2022/nfm1.lean b/doc/examples/NFM2022/nfm1.lean new file mode 100644 index 0000000000..6126f09adc --- /dev/null +++ b/doc/examples/NFM2022/nfm1.lean @@ -0,0 +1,20 @@ +#eval "hello" ++ " " ++ "world" +-- "hello world" + +#check true +-- Bool + +def x := 10 + +#eval x + 2 +-- 12 + +def double (x : Int) := 2*x + +#eval double 3 +-- 6 +#check double +-- Int → Int +example : double 4 = 8 := rfl + + diff --git a/doc/examples/NFM2022/nfm10.lean b/doc/examples/NFM2022/nfm10.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm11.lean b/doc/examples/NFM2022/nfm11.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm12.lean b/doc/examples/NFM2022/nfm12.lean new file mode 100644 index 0000000000..4c6b325197 --- /dev/null +++ b/doc/examples/NFM2022/nfm12.lean @@ -0,0 +1,27 @@ +namespace Example + +class ToString (α : Type u) where + toString : α → String + +#check @ToString.toString +-- {α : Type u_1} → [self : ToString α] → α → String + +instance : ToString String where + toString s := s + +instance : ToString Bool where + toString b := if b then "true" else "false" + +#eval ToString.toString "hello" +export ToString (toString) +#eval toString true +-- "true" +#eval toString (true, "hello") -- Error + +instance [ToString α] [ToString β] : ToString (α × β) where + toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")" + +#eval toString (true, "hello") +-- "(true, hello)" + +end Example diff --git a/doc/examples/NFM2022/nfm13.lean b/doc/examples/NFM2022/nfm13.lean new file mode 100644 index 0000000000..42eaad5f43 --- /dev/null +++ b/doc/examples/NFM2022/nfm13.lean @@ -0,0 +1,20 @@ +namespace Example + +class Mul (α : Type u) where + mul : α → α → α + +infixl:70 " * " => Mul.mul + +class Semigroup (α : Type u) extends Mul α where + mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c) + +class Functor (f : Type u → Type v) : Type (max (u+1) v) where + map : (α → β) → f α → f β + +infixr:100 " <$> " => Functor.map + +class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where + id_map (x : f α) : id <$> x = x + comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x + +end Example diff --git a/doc/examples/NFM2022/nfm14.lean b/doc/examples/NFM2022/nfm14.lean new file mode 100644 index 0000000000..c47488695a --- /dev/null +++ b/doc/examples/NFM2022/nfm14.lean @@ -0,0 +1,13 @@ +example : p → q → p ∧ q ∧ p := by + intro hp hq + apply And.intro + exact hp + apply And.intro + exact hq + exact hp + +example : p → q → p ∧ q ∧ p := by + intro hp hq + apply And.intro + exact hp + exact And.intro hq hp diff --git a/doc/examples/NFM2022/nfm15.lean b/doc/examples/NFM2022/nfm15.lean new file mode 100644 index 0000000000..d8fdb54ad6 --- /dev/null +++ b/doc/examples/NFM2022/nfm15.lean @@ -0,0 +1,17 @@ + +example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by + intro h + match h with + | Exists.intro w (And.intro hp hq) => exact Exists.intro w (And.intro hq hp) + +example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by + intro (Exists.intro _ (And.intro hp hq)) + exact Exists.intro _ (And.intro hq hp) + +example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by + intro (.intro _ (.intro hp hq)) + exact .intro _ (.intro hq hp) + +example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by + intro ⟨_, hp, hq⟩ + exact ⟨_, hq, hp⟩ diff --git a/doc/examples/NFM2022/nfm16.lean b/doc/examples/NFM2022/nfm16.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm17.lean b/doc/examples/NFM2022/nfm17.lean new file mode 100644 index 0000000000..21591b45cd --- /dev/null +++ b/doc/examples/NFM2022/nfm17.lean @@ -0,0 +1,17 @@ +example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by + intro h + cases h with + | intro x hpq => + cases hpq with + | intro hp hq => + exists x + +example : p ∧ q → q ∧ p := by + intro p + cases p + constructor <;> assumption + +example : p ∧ ¬ p → q := by + intro h + cases h + contradiction diff --git a/doc/examples/NFM2022/nfm18.lean b/doc/examples/NFM2022/nfm18.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm19.lean b/doc/examples/NFM2022/nfm19.lean new file mode 100644 index 0000000000..a6e6ea6678 --- /dev/null +++ b/doc/examples/NFM2022/nfm19.lean @@ -0,0 +1,8 @@ +example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by + intros + repeat (any_goals constructor) + all_goals assumption + +example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by + intros + repeat (any_goals (first | assumption | constructor)) diff --git a/doc/examples/NFM2022/nfm2.lean b/doc/examples/NFM2022/nfm2.lean new file mode 100644 index 0000000000..fa9f1df0c2 --- /dev/null +++ b/doc/examples/NFM2022/nfm2.lean @@ -0,0 +1,12 @@ +def twice (f : Nat → Nat) (a : Nat) := + f (f a) + +#check twice +-- (Nat → Nat) → Nat → Nat + +#eval twice (fun x => x + 2) 10 + +theorem twice_add_2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl + +-- `(· + 2)` is syntax sugar for `(fun x => x + 2)`. +#eval twice (· + 2) 10 diff --git a/doc/examples/NFM2022/nfm20.lean b/doc/examples/NFM2022/nfm20.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm21.lean b/doc/examples/NFM2022/nfm21.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm22.lean b/doc/examples/NFM2022/nfm22.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm23.lean b/doc/examples/NFM2022/nfm23.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm24.lean b/doc/examples/NFM2022/nfm24.lean new file mode 100644 index 0000000000..2ff564d7cf --- /dev/null +++ b/doc/examples/NFM2022/nfm24.lean @@ -0,0 +1,9 @@ + + +example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by + induction as with + | nil => rfl + | cons x xs ih => simp [List.concat, ih] + +example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by + induction as <;> simp! [*] diff --git a/doc/examples/NFM2022/nfm3.lean b/doc/examples/NFM2022/nfm3.lean new file mode 100644 index 0000000000..8b22076865 --- /dev/null +++ b/doc/examples/NFM2022/nfm3.lean @@ -0,0 +1,55 @@ +inductive Weekday where + | sunday | monday | tuesday | wednesday + | thursday | friday | saturday + +#check Weekday.sunday +-- Weekday + +open Weekday +#check sunday + +def natOfWeekday (d : Weekday) : Nat := + match d with + | sunday => 1 + | monday => 2 + | tuesday => 3 + | wednesday => 4 + | thursday => 5 + | friday => 6 + | saturday => 7 + +def Weekday.next (d : Weekday) : Weekday := + match d with + | sunday => monday + | monday => tuesday + | tuesday => wednesday + | wednesday => thursday + | thursday => friday + | friday => saturday + | saturday => sunday + +def Weekday.previous : Weekday → Weekday + | sunday => saturday + | monday => sunday + | tuesday => monday + | wednesday => tuesday + | thursday => wednesday + | friday => thursday + | saturday => friday + +theorem Weekday.next_previous (d : Weekday) : d.next.previous = d := + match d with + | sunday => rfl + | monday => rfl + | tuesday => rfl + | wednesday => rfl + | thursday => rfl + | friday => rfl + | saturday => rfl + +theorem Weekday.next_previous' (d : Weekday) : d.next.previous = d := by -- switch to tactic mode + cases d -- Creates 7 goals + rfl; rfl; rfl; rfl; rfl; rfl; rfl + +theorem Weekday.next_previous'' (d : Weekday) : d.next.previous = d := by + cases d <;> rfl diff --git a/doc/examples/NFM2022/nfm4.lean b/doc/examples/NFM2022/nfm4.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm5.lean b/doc/examples/NFM2022/nfm5.lean new file mode 100644 index 0000000000..676526371e --- /dev/null +++ b/doc/examples/NFM2022/nfm5.lean @@ -0,0 +1,19 @@ +def f (α β : Sort u) (a : α) (b : β) : α := a + +#eval f Nat String 1 "hello" +-- 1 + +def g {α β : Sort u} (a : α) (b : β) : α := a + +#eval g 1 "hello" + +def h (a : α) (b : β) : α := a + +#check g +-- ?m.1 → ?m.2 → ?m.1 +#check @g +-- {α β : Sort u} → α → β → α +#check @h +-- {α : Sort u_1} → {β : Sort u_2} → α → β → α +#check g (α := Nat) (β := String) +-- Nat → String → Nat diff --git a/doc/examples/NFM2022/nfm6.lean b/doc/examples/NFM2022/nfm6.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/doc/examples/NFM2022/nfm7.lean b/doc/examples/NFM2022/nfm7.lean new file mode 100644 index 0000000000..d37463c700 --- /dev/null +++ b/doc/examples/NFM2022/nfm7.lean @@ -0,0 +1,23 @@ +#print Nat -- Nat is an inductive datatype + +def fib (n : Nat) : Nat := + match n with + | 0 => 1 + | 1 => 1 + | n+2 => fib (n+1) + fib n + +example : fib 5 = 8 := rfl + +example : fib (n+2) = fib (n+1) + fib n := rfl + +#print fib +/- +def fib : Nat → Nat := +fun n => + Nat.brecOn n fun n f => + (match (motive := (n : Nat) → Nat.below n → Nat) n with + | 0 => fun x => 1 + | 1 => fun x => 1 + | Nat.succ (Nat.succ n) => fun x => x.fst.fst + x.fst.snd.fst.fst) + f +-/ diff --git a/doc/examples/NFM2022/nfm8.lean b/doc/examples/NFM2022/nfm8.lean new file mode 100644 index 0000000000..78ecadc640 --- /dev/null +++ b/doc/examples/NFM2022/nfm8.lean @@ -0,0 +1,17 @@ +def sum (a : Array Int) : Int := + let rec go (i : Nat) := + if i < a.size then + a[i] + go (i+1) + else + 0 + go 0 +termination_by go i => a.size - i + +set_option pp.proofs true +#print sum.go +/- +def sum.go : Array Int → Nat → Int := +fun a => + WellFounded.fix (sum.go.proof_1 a) fun i a_1 => + if h : i < Array.size a then Array.getOp a i + a_1 (i + 1) (sum.go.proof_2 a i h) else 0 +-/ diff --git a/doc/examples/NFM2022/nfm9.lean b/doc/examples/NFM2022/nfm9.lean new file mode 100644 index 0000000000..8a5e2490cf --- /dev/null +++ b/doc/examples/NFM2022/nfm9.lean @@ -0,0 +1,39 @@ +inductive Term where + | const : String → Term + | app : String → List Term → Term + +namespace Term +mutual + def numConsts : Term → Nat + | const _ => 1 + | app _ cs => numConstsLst cs + def numConstsLst : List Term → Nat + | [] => 0 + | c :: cs => numConsts c + numConstsLst cs +end + +mutual + def replaceConst (a b : String) : Term → Term + | const c => if a = c then const b else const c + | app f cs => app f (replaceConstLst a b cs) + + def replaceConstLst (a b : String) : List Term → List Term + | [] => [] + | c :: cs => replaceConst a b c :: replaceConstLst a b cs +end + +mutual + theorem numConsts_replaceConst (a b : String) (e : Term) + : numConsts (replaceConst a b e) = numConsts e := by + match e with + | const c => simp [replaceConst]; split <;> simp [numConsts] + | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs] + + theorem numConsts_replaceConstLst (a b : String) (es : List Term) + : numConstsLst (replaceConstLst a b es) = numConstsLst es := by + match es with + | [] => simp [replaceConstLst, numConstsLst] + | c :: cs => + simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c, + numConsts_replaceConstLst a b cs] +end