1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

Lean
    [#Microsoft research]
    [programming language]

    A theorem prover and programming language.

    It is based on the Calculus of
    Constructions with inductive types.

    Lean has a number of features that
    differentiate it from other interactive
    theorem provers.

    Lean can be compiled to JavaScript and
    accessed in a web browser.

    It has native support for Unicode symbols.

1
2
3
4
5
6
7
8

Lean 4
Lean 4 is under development. There are no
official releases yet.

Lean 3
These are the official releases of Lean 3. For
the extended community version of Lean 3,
please see leanprover-community/lean.

1

cd "$DUMP/programs"; wget "https://github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz"

1

lean --help

1

man +/"ctest - CTest Command-Line Reference" "ctest(1)"

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

NAME
       ctest - CTest Command-Line Reference

SYNOPSIS
          ctest [<options>]

DESCRIPTION
       The  "ctest"  executable  is  the  CMake test driver program.
       CMake-generated build trees created for projects that use the
       ENABLE_TESTING  and  ADD_TEST  commands have testing support.
       This program will run the tests and report results.

1

cd "$MYGIT/leanprover/lean"; tp find-here-path "*exampl*"

1
2
3
4
5

open expr tactic

example : false := by do
n ← mk_fresh_name,
apply (local_const n n binder_info.default (const ``false []))

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

universe variables u
variables (A : Type u) [H : inhabited A] (x : A)
include H

definition foo := x
#check foo  -- A and x are explicit

variables {A x}
definition foo' := x
#check @foo' -- A is explicit, x is implicit

open nat

#check foo nat 10

definition test : foo' = (10:nat) := rfl

set_option pp.implicit true
#print test

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

-- Inductive propositions.

-- Example 1: even numbers.

-- inductive definition of "is_even" predicate on the real numbers
inductive is_even : ℕ → Prop
| even0 : is_even 0
| evenSS : ∀ n : ℕ, is_even n → is_even (n + 2)

open is_even

theorem four_is_even : is_even 4 :=
begin
  -- goal now `is_even 4`
  apply evenSS,
  -- goal now `is_even 2`
  apply evenSS,
  -- goal now `is_even 0`
  exact even0
end

-- can do it with functions too
theorem six_is_even : is_even 6 := evenSS 4 $ evenSS 2 $ evenSS 0 even0

theorem one_is_not_even : ¬ (is_even 1) :=
begin
  intro H,
  -- H : is_even 1
  -- clearly H can not have been proved using either even0 or evenSS
  -- so when we do this
  cases H,
  -- there are no cases left, so the proof is over!
end

-- cases can also be used to pull down higher odd numbers
theorem five_is_not_even : ¬ (is_even 5) :=
begin
  intro H5,
  cases H5 with _ H3,
  cases H3 with _ H1,
  cases H1,
end

-- example of usage
lemma even_iff_SS_even (n : ℕ) : is_even n ↔ is_even (n + 2) :=
begin
  split,
  { -- easy way
    exact evenSS n,
  },
  -- other way a bit trickier
  intro HSSn,
  cases HSSn with _ Hn,
  assumption
end

-- Example 2: the Collatz conjecture.

/-- collatz n means the collatz conjecture is true for n -/
inductive collatz : ℕ → Prop
| coll0 : collatz 0
| coll1 : collatz 1
| coll_even : ∀ n : ℕ, collatz n → collatz (2 * n)
| coll_odd : ∀ n : ℕ , collatz (6 * n + 4) → collatz (2 * n + 1)

open collatz


theorem coll10 : collatz 10 :=
begin
apply coll_even 5,
apply coll_odd 2,
apply coll_even 8,
apply coll_even 4,
apply coll_even 2,
apply coll_even 1,
apply coll1
end

theorem coll10' : collatz 10 :=
  coll_even 5 $ coll_odd 2 $ coll_even 8 $ coll_even 4 $ coll_even 2 $ coll_even 1 coll1

-- if m is odd then 3m+1 is always even, so we can go from m=2n+1 to 6n+4 and then to 3n+2 in one step.
lemma coll_odd' (n : ℕ) : collatz (3 * n + 2) → collatz (2 * n + 1) :=
begin
  intro H3n2,
  apply coll_odd,
  -- unfortunately applying coll_even will tell us about collatz (2 * (3 * n + 2))
  -- rather than collatz (6 * n + 4), so let's fix this
  rw (show 6 * n + 4 = 2 * (3 * n + 2), by rw [mul_add,←mul_assoc];refl),
  -- with tactic.ring imported from mathlib this line could just be
  --  rw (show 6 * n + 4 = 2 * (3 * n + 2), by ring),

  apply coll_even,
  assumption
end

-- now we can go a bit quicker
theorem coll10'' : collatz 10 :=
begin
  apply coll_even 5,
  apply coll_odd' 2,
  apply coll_even 4,
  apply coll_even 2,
  apply coll_even 1,
  apply coll1
end

-- Of course one should really be using a home-grown tactic to figure out which
-- of coll_even, coll_odd and coll1 to apply next.

/- this is the Collatz conjecture -/
-- theorem collatz_conjecture : ∀ n : ℕ, collatz n := sorry
-- Nobody knows how to prove this.