Types and Programming Languages

Stream: new members

[Patrick Thomas]

Did I set this up right? I'm having some trouble proving it.

-- Types and Programming Languages Kindle Edition by Benjamin C. Pierce (Author) Format: Kindle Edition
-- Theorem 3.3.4

inductive term : Type
  | true
  | false
  | zero
  | succ (t1 : term)
  | pred (t1 : term)
  | iszero (t1 : term)
  | ite (t1 : term) (t2 : term) (t3 : term)


def size : term -> nat
  | term.true := 1
  | term.false := 1
  | term.zero := 1
  | (term.succ t1) := (size t1) + 1
  | (term.pred t1) := (size t1) + 1
  | (term.iszero t1) := (size t1) + 1
  | (term.ite t1 t2 t3) := (size t1) + (size t2) + (size t3) + 1


-- principle of complete mathematical induction
axiom PCI :
forall P : nat -> Prop,
(forall m : nat, (forall i : nat, i < m -> P i) -> P m) ->
forall n : nat, P n


-- induction on size
theorem IOS :
forall P : term -> Prop,
(forall s : term, (forall r : term, size r < size s -> P r) -> P s) ->
forall t : term, P t :=
begin
intros P,
let Q := fun (n : nat), forall s : term, (size s = n) -> P s,
have s1 : (forall m : nat, (forall i : nat, i < m -> Q i) -> Q m) -> forall n : nat, Q n, from PCI Q,
sorry
end

[Mario Carneiro]

here's a more leanified version, and a good start on the problem. I removed the definition Q because it obscures more than it helps in this proof.

-- principle of complete mathematical induction
theorem PCI (P : ℕ → Prop)
  (H : ∀ m : ℕ, (∀ i, i < m → P i) → P m)
  (n : ℕ) : P n :=
nat.strong_induction_on n H

-- induction on size
theorem IOS (P : term → Prop)
  (H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
  (t : term) : P t :=
begin
  refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ _ t rfl,
  dsimp only,
  intros m ih s e,
  sorry
end

[Patrick Thomas]

What is the refine tactic doing?

[Johan Commelin]

It is like exact, but you can leave some holes using _. If Lean can't figure out what to put in place of those _, it doesn't throw an error, but creates a new goal instead.

[Patrick Thomas]

So is everything after PCI in that line, the hypotheses to PCI?

[Johan Commelin]

yup

[Patrick Thomas]

Where do the t and the rfl line up?

[Mario Carneiro]

PCI has three arguments, but the result is P n, and since in this case we substituted λ (n : nat), ∀ s : term, size s = n → P s for P, the result after substituting the first three arguments is ∀ s : term, size s = ?n → P s and we have space to add two more arguments

[Mario Carneiro]

here's a more broken down version of the first line:

  have : ∀ (s : term), size s = size t → P s :=
    PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ (size t),
  refine this t rfl,

[Patrick Thomas]

I see. Thank you.

[Patrick Thomas]

Thank you!

-- induction on size
theorem IOS (P : term → Prop)
  (H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
  (t : term) : P t :=
begin
  refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ _ t rfl,
  dsimp only,
  intros m ih s e,
  apply H,
  intros r a,
  apply (ih (size r)),
  rw <- e,
  apply a,
  refl
end

[Mario Carneiro]

Good job. Now, the cheating way:

theorem IOS (P : term → Prop)
  (H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
  (t : term) : P t :=
(measure_wf size).induction t H

[Mario Carneiro]

(There are even more cheating ways when you notice that size is the same as term.sizeof, and indeed this particular theorem is applied automatically by lean when you write functions by well founded recursion using the equation compiler.)

[Mario Carneiro]

here's a golfy proof more similar to yours:

theorem IOS (P : term → Prop)
  (H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
  (t : term) : P t :=
begin
  refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ (size t) t rfl,
  rintro m ih s rfl,
  refine H _ (λ r h, ih _ h r rfl),
end

[Patrick Thomas]

The book defines structural induction as:

If, for each term s,
given P(r) for all immediate subterms r of s we can show P(s),
then P(s) holds for all s.

How does one formalize this and show that it follows from weak mathematical induction? Do I define a function is_immediate_subterm : term -> term -> Prop and then:

forall P : term -> Prop,
(forall s : term, (forall r : term, (is_immediate_subterm r s) -> P r) -> P s) ->
forall t : term, P t

Also, I'm not sure how to go about defining a function f : term -> nat such that f s = (f r) + 1 iff (is_immediate_subterm r s) to use to show that it follows from weak mathematical induction, if that is what I need to do.

[Chris B]

There might be an even more primitive way of doing this in mathlib, but in core this is done with acc and its recursor, then measure_wf, and sizeof_measure_wf, which are other helper functions/lemmas in that file. sizeof is automatically generated for inductives, I think the general rule is just that forall a, sizeof(ctor(a)) = sizeof(a) + 1.

[Chris B]

Actually it looks like sizeof is defined manually for some primitives, like list and option.

protected def option.sizeof {α : Type u} [has_sizeof α] : option α → nat
| none     := 1
| (some a) := 1 + sizeof a

protected def list.sizeof {α : Type u} [has_sizeof α] : list α → nat
| list.nil        := 1
| (list.cons a l) := 1 + sizeof a + list.sizeof l

[Mario Carneiro]

That's just because they are needed during bootstrapping. They would normally be created automatically but the sizeof framework isn't yet set up when those inductives are introduced.

[Mario Carneiro]

Patrick Thomas said:

The book defines structural induction as:

If, for each term s,
given P(r) for all immediate subterms r of s we can show P(s),
then P(s) holds for all s.

How does one formalize this and show that it follows from weak mathematical induction?

In lean, this is the wrong way around. Structural induction is primitive; it is true by the axioms associated to each inductive type. Weak induction on nat is a special case of structural induction, as is induction on acc which yields well founded recursion, which proves strong induction using sizeof.

[Mario Carneiro]

The shape of each structural induction theorem looks a little different since it depends on how the inductive is defined. Try #print term.rec to see what it looks like for term.

[Patrick Thomas]

Can it still be proven this way around?

[Mario Carneiro]

The easiest way to prove a theorem using is_immediate_subterm is to define it as an inductive family and then prove it using term.rec

[Patrick Thomas]

I guess I'm trying to do the exercise in the book, to prove that it follows from weak mathematical induction, similar to the earlier proof using size.

[Mario Carneiro]

It's not possible to do this from weak nat recursion directly, because one term can have two immediate subterm of different heights. For example ite true (succ zero) zero yields the relations:

f (ite true (succ zero) zero) = f (succ zero) + 1
f (ite true (succ zero) zero) = f zero + 1
f (succ zero) = f zero + 1

which are clearly unsolvable. The easy way to derive this using PCI is to just use strong recursion on terms and use that "immediate subterm" implies sizeof strict inequality.

[Patrick Thomas]

I'm sorry, what does strong recursion on terms mean?
Do you mean, define the function is_immediate_subterm: term -> term -> Prop, then prove forall r, s : term, is_immediate_subterm r s -> size r < size s. Then proceed as in the earlier proof?

[Patrick Thomas]

Like this?

constant term : Type

constant size : term → ℕ

constant is_immediate_subterm : term → term → Prop

lemma subterm_size (r s : term) : is_immediate_subterm r s -> size r < size s := sorry

-- principle of complete mathematical induction
theorem PCI (P : ℕ → Prop)
  (H : ∀ m : ℕ, (∀ i, i < m → P i) → P m)
  (n : ℕ) : P n :=
nat.strong_induction_on n H

theorem SI (P : term → Prop)
  (H : ∀ s : term, (∀ r : term, is_immediate_subterm r s → P r) → P s)
  (t : term) : P t :=
begin
  refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ _ t rfl,
  dsimp only,
  intros m ih s e,
  apply H,
  intros r a,
  apply (ih (size r)),
  rw <- e,
  apply (subterm_size r s a),
  refl
end

[Patrick Thomas]

Thank you. I thought it was more complicated and was heading in the wrong direction.

[Mario Carneiro]

You can actually just apply the previous theorem instead of replaying it

[Patrick Thomas]

Yeah, that probably would have been simpler :)

[Patrick Thomas]

3.2.1 Definition [Terms, Inductively]: The set of terms is the smallest set $T$ such that

1. {true, false, 0} $\subseteq T$;
2. if $t_{1} \in T$, then {succ $t_{1}$, pred $t_{1}$, iszero $t_{1}$} $\subseteq T$;
3. if $t_{1} \in T$, $t_{2} \in T$, and $t_{3} \in T$, then if $t_{1}$ then $t_{2}$ else $t_{3}$ $\in T$.

I think the equivalent of Definition 3.2.1 in Lean is

inductive term : Type
  | true
  | false
  | zero
  | succ (t1 : term)
  | pred (t1 : term)
  | iszero (t1 : term)
  | ite (t1 : term) (t2 : term) (t3 : term)

In a similar manner, Is there an equivalent of Definition 3.2.3 in Lean? By equivalent I mean as a translation from set theory to type theory, not the fact that $S$ and $T$ are the same set.

3.2.3 Definition [Terms, Concretely]: For each natural number $i$, define a set $S_{i}$ as follows:
$S_{0} = \empty$
$S_{i+1}$ = {true, false, 0} $\cup$ {succ $t_{1}$, pred $t_{1}$, iszero $t_{1} | t_{1} \in S_{i}$} $\cup$ {if $t_{1}$ then $t_{2}$ else $t_{3}$| $t_{1}, t_{2}, t_{3} \in S_{i}$}.
Finally, let $S = \bigcup S_{i}$.

[Patrick Thomas]

Maybe the Lean definition I gave goes with definition 3.2.3 and the question is about an equivalent Lean definition for 3.2.1? I'm not certain.

[Reid Barton]

The Lean translation looks good. Definition 3.2.3 is a standard way in set theory to justify Definition 3.2.1, which is not complete as it stands (because a priori there might not be any set $T$ with this property). You could try to imitate Definition 3.2.3 in Lean, but it would be awkward and it's probably more sensible to just accept that the basic building blocks of type theory are different from in set theory.

[Patrick Thomas]

I see. Thank you!

[Patrick Thomas]

Something like this perhaps?

import data.set
open set


-- Terms, Inductively

constant T : set string

def rule_1 (S : set string) := {"true", "false", "zero"} ⊆ S
def rule_2 (S : set string) := forall t1 : string, t1 ∈ S → {"succ" ++ t1, "pred" ++ t1, "iszero" ++ t1} ⊆ S
def rule_3 (S : set string) := forall t1 t2 t3 : string, "ite" ++ t1 ++ t2 ++ t3 ∈ S

constant holds : rule_1 T → rule_2 T → rule_3 T
constant smallest : ∀ S : set string, rule_1 S → rule_2 S → rule_3 S → T ⊆ S


-- Terms, Concretely

def f : ℕ → set string
  | nat.zero := ∅
  | (nat.succ i) :=
      {"true", "false", "zero"}
      ∪ {("succ" ++ t1) | t1 ∈ f i} ∪ {("pred" ++ t1) | t1 ∈ f i} ∪ {("iszero" ++ t1) | t1 ∈ f i}
      ∪ {("ite" ++ t1 ++ t2 ++ t3) | t1 t2 t3 ∈ f i}

def S := ⋃ i : ℕ, f i

example : T = S := sorry

[Kyle Miller]

It seems you've forgotten spaces between terms. Also, holds seems odd (maybe you meant conjunctions?), and rather than introducing smallest and T as constants, you can prove that S is smallest as a theorem, replacing the example.

One downside with strings is that to be able to use them as terms you have to go through the effort of parsing them.

[Patrick Thomas]

What would be a good alternative to strings?

[Patrick Thomas]

Yes, you are right, I should have defined holds with conjunctions.

[Kyle Miller]

One option is to add enough parenthesis so parsing is easy (though you still would want to parse). It can also be nice to add some functions to make sure you generate the correct syntax.

import data.set
open set

namespace pre_term
def true := "true"
def false := "false"
def zero := "zero"
def succ (s : string) := "(succ " ++ s ++ ")"
def pred (s : string) := "(pred " ++ s ++ ")"
def iszero (s : string) := "(iszero " ++ s ++ ")"
def ite (s t u : string) := "(ite " ++ s ++ " " ++ t ++ " " ++ u ++ ")"
end pre_term

def rule_1 (S : set string) : set string := {pre_term.true, pre_term.false, pre_term.zero}

def rule_2 (S : set string) : set string :=
{(pre_term.succ t1) | t1 ∈ S} ∪ {(pre_term.pred t1) | t1 ∈ S} ∪ {(pre_term.iszero t1) | t1 ∈ S}

def rule_3 (S : set string) : set string := {(pre_term.ite t1 t2 t3) | t1 t2 t3 ∈ S}

def f : ℕ → set string
  | nat.zero := ∅
  | (nat.succ i) := rule_1 (f i) ∪ rule_2 (f i) ∪ rule_3 (f i)

def S := ⋃ i : ℕ, f i

theorem holds : rule_1 S ⊆ S ∧ rule_2 S ⊆ S ∧ rule_3 S ⊆ S := sorry
theorem smallest : ∀ (T : set string), rule_1 T ⊆ T → rule_2 T ⊆ T → rule_3 T ⊆ T → S ⊆ T := sorry

[Kyle Miller]

And then you could go on to create the subtype of those strings that are in S and make all the constructors:

def term : Type := S -- this is the set coerced to a type

namespace term
def true : term := ⟨pre_term.true, begin use (f 1), simp [f, rule_1], use 1, refl, end⟩ -- (not a very pretty proof)
def false : term := sorry
def zero : term := sorry
def succ (t1 : term) : term := sorry
def pred (t1 : term) : term := sorry
def iszero (t1 : term) : term := sorry
def ite (t1 t2 t3 : term) : term := sorry
end term

[Patrick Thomas]

Cool. Thank you!

[Kyle Miller]

This is another setup that I'd expect to be somewhat easier to parse (and by "parse" I mean writing the recursor). It uses lists of symbols:

import data.set
open set

inductive symb
| true | false | zero | succ | pred | iszero | ite

namespace pre_term
def true := [symb.true]
def false := [symb.false]
def zero := [symb.zero]
def succ (s : list symb) := [symb.succ] ++ s
def pred (s : list symb) := [symb.pred] ++ s
def iszero (s : list symb) := [symb.iszero] ++ s
def ite (s t u : list symb) := [symb.ite] ++ s ++ t ++ u
end pre_term

def rule_1 : set (list symb) := {pre_term.true, pre_term.false, pre_term.zero}

def rule_2 (S : set (list symb)) : set (list symb) :=
{(pre_term.succ t1) | t1 ∈ S} ∪ {(pre_term.pred t1) | t1 ∈ S} ∪ {(pre_term.iszero t1) | t1 ∈ S}

def rule_3 (S : set (list symb)) : set (list symb) := {(pre_term.ite t1 t2 t3) | t1 t2 t3 ∈ S}

def f : ℕ → set (list symb)
  | nat.zero := ∅
  | (nat.succ i) := rule_1 ∪ rule_2 (f i) ∪ rule_3 (f i)

def S := ⋃ i : ℕ, f i

theorem holds : rule_1 ⊆ S ∧ rule_2 S ⊆ S ∧ rule_3 S ⊆ S := sorry
theorem smallest : ∀ (T : set (list symb)), rule_1 ⊆ T → rule_2 T ⊆ T → rule_3 T ⊆ T → S ⊆ T := sorry

def term : Type := S

namespace term
def true : term := ⟨pre_term.true, begin use (f 1), simp [f, rule_1], use 1, refl, end⟩
def false : term := sorry
def zero : term := sorry
def succ (t1 : term) : term := sorry
def pred (t1 : term) : term := sorry
def iszero (t1 : term) : term := sorry
def ite (t1 t2 t3 : term) : term := sorry
end term

[Patrick Thomas]

Nice!

[Patrick Thomas]

Going back to the discussion on induction; in set theory, the principle of mathematical induction follows from the well ordering principle, and is equivalent to complete mathematical induction. In addition, we have just shown that structural induction follows from complete mathematical induction. Do all forms of induction in set theory then follow from the well ordering principle? What about induction on inductively defined propositions? Can I formalize and show this in Lean?

[Patrick Thomas]

I'm not sure how to formalize the well ordering principle in Lean, or what a generic formalization of induction on inductively defined propositions would look like, in a vein similar to:

forall P : nat -> Prop,
(forall m : nat, (forall i : nat, i < m -> P i) -> P m) ->
forall n : nat, P n

[Patrick Thomas]

That is, I think we have that all of these are equivalent:

-- Principle of Mathematical Induction
def PMI :=
∀ P : ℕ → Prop,
P 0 ∧ (∀ m : ℕ, P m → P (m + 1)) →
∀ n : ℕ, P n


-- Principle of Induction from a Starting Point
def SP :=
∀ P : ℕ → Prop,
∀ m : ℕ,
P m ∧ (∀ i : ℕ, i ≥ m → (P i → P (i + 1))) →
∀ n : ℕ, n ≥ m → P n


-- Principle of Complete Induction
def PCI :=
∀ P : ℕ → Prop,
(∀ m : ℕ, (∀ i : ℕ, i < m → P i) → P m) →
∀ n : ℕ, P n


-- Structural induction

constant term : Type
constant size : term -> ℕ
constant is_immediate_subterm : term -> term -> Prop

lemma subterm_size : ∀ r s : term, is_immediate_subterm r s → size r < size s := sorry

def SI :=
∀ P : term → Prop,
(∀ s : term, (∀ r : term, is_immediate_subterm r s → P r) → P s) ->
∀ t : term, P t

How do we formalize the well ordering principle to show that they all follow from it, and also give a similar formal definition of induction over an inductively defined proposition and show that it follows as well.

[Eric Wieser]

Proving that PMI follows from well-ordering is as interesting as showing true follows from it, because PMI is true by definition of nat.rec

[Eric Wieser]

If you want to prove the recursor of nat (PMI) follows from something more fundamental, then you can't use the built-in definition of nat or any similar inductive definition of nat because such a definition introduces PMI as an "axiom".

[Patrick Thomas]

I guess I'm not sure how to define nat in Lean in set theoretical terms, and figured I just wouldn't use that fact.

[Patrick Thomas]

But I would be interested in seeing it in Lean in set theoretical terms.

[Patrick Thomas]

Or just how to add in induction on inductively defined propositions with it as it is.

[Patrick Thomas]

Something like?

namespace hidden

constant nat : Type
constant le : nat → nat → Prop
constant lt : nat → nat → Prop

def WOP : Prop := ∀ s : set nat, ∃ t : nat, t ∈ s → ∃ u : nat, u ∈ s ∧ ∀ v : nat, v ∈ s → le u v

def PCI : Prop :=
∀ P : nat → Prop,
(∀ m : nat, (∀ i : nat, lt i m → P i) → P m) →
∀ n : nat, P n

example : WOP → PCI := sorry

end hidden

[Eric Wieser]

That looks unprovable because you have nothing saying how lt and le interact.

[Patrick Thomas]

I was just throwing it together leaving them to be defined.

[Patrick Thomas]

The question I am most interested in, is how to similarly formalize and show (if it holds true) that induction on inductively defined propositions is related to mathematical induction.

[Patrick Thomas]

For example, what is the form of the induction principle on step and can it be related to the principle of mathematical induction:

inductive term : Type
  | true
  | false
  | zero
  | succ (t1 : term)
  | pred (t1 : term)
  | iszero (t1 : term)
  | ite (t1 : term) (t2 : term) (t3 : term)

-- step x y means that (x, y) is in the evaluation relation
inductive step : term → term → Prop
  | e_if_true (t2 t3 : term) :
    step (term.ite term.true t2 t3) t2
  | e_if_false (t2 t3 : term) :
    step (term.ite term.false t2 t3) t3
  | e_if (t1 t1' t2 t3 : term) :
    step t1 t1' → step (term.ite t1 t2 t3) (term.ite t1' t2 t3)

[Eric Wieser]

You can ask lean for the "form of induction principle on step" with #check @step.rec

[Patrick Thomas]

Can that induction principle be shown to follow from one of the others?

[Eric Wieser]

If it can be shown, you can't write the proof in lean itself while keeping that definition of step.

[Eric Wieser]

You'd need to formalize the rules of inductive types in lean itself, and describe step in that language in order to use Lean to show what you're asking.

[Patrick Thomas]

I am guessing that there is an axiom in Lean that all of the various forms of induction in Lean follow from?

[Eric Wieser]

Every time you use the keyword inductive or structure or class you are essentially introducing a new recursor "axiom" (but not axiom) into lean

[Patrick Thomas]

What ensures that they are permissible?

[Eric Wieser]

The rules that dictate what is and is not a valid (non-meta)inductive type ensure they are permissible. Lean itself does not provide a proof that they are permissible, that's the foundation you as the user are putting your trust upon.

[Eric Wieser]

I would expect the paper on lean itself to provide ample references to how exactly that foundation is justified mathematically; but I think those were already linked in your other thread?

[Patrick Thomas]

I see.

[One An]

Hello, I'm trying to enter tactic mode, but when I type begin, it shows "unknown identifier 'begin'. Why does it say that begin is an unknown identifier. It does seem like it recognize "end" because it says "invalid 'end', insufficient scopes." Thank you for the help\

[Kyle Miller]

Are you using Lean 3 or Lean 4? If Lean 4, then the new syntax is just by, not begin ... end.

If Lean 3, do you have an example you can paste here that shows the error? (You can put the code between triple #backticks to get it to format nicely)

[One An]

begin
  apply and.intro,
  exact hp,
  apply and.intro,
  exact hq,
  exact hp
end

[One An]

how do i use the "by" syntax? is there a tutorial? I will try using lean 4 instead

[Kyle Miller]

Is that your complete example? You seem to not have included enough of your file -- where's the code for the theorem you're proving?

[One An]

oh sorry, i dont know why it didn't copy for some reason

[One An]

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=
begin
  apply and.intro,
  exact hp,
  apply and.intro,
  exact hq,
  exact hp
end

[One An]

or theres this another example

[One An]

variables (P  Q R : Prop)
lemma identity : P /to P :=
begin
intro hp
exact hp
end

[One An]

I changed to lean 4 and managed to make it work by using "by" instead!

[Kyle Miller]

In Lean 3 this works:

variables (P  Q R : Prop)
lemma identity : P → P :=
begin
  intro hp,
  exact hp
end

[Kyle Miller]

In Lean 4 you get the error you're describing:

variable (P  Q R : Prop)
lemma identity : P → P :=
begin -- unknown identifier 'begin'
  intro hp,
  exact hp
end

[Kyle Miller]

You must have been using Lean 4 to get this error

[Kyle Miller]

Here's the valid Lean 4 code:

variable (P Q R : Prop)
theorem identity : P → P := by
  intro hp
  exact hp

[One An]

image.png
that still doesnt work for lean 4 some reason. Am I doing something wrong?

[Kyle Miller]

I just changed it to work without any imports. Now it's theorem

[Kyle Miller]

If you have Mathlib set up, you can do import Mathlib to get lemma, which is just a theorem as far as Lean is concerned

[One An]

How do i import it? Do I do it through bash? Also, do you recommend sticking with lean 4 or going back and downloading lean 3?

[One An]

Thank you for helping

[One An]

Also, how do i make the goal appear on the left? I've seen some people do it and I'm not sure how

[Damiano Testa]

If your project has Mathlib as a dependecy, then you can write at the beginning of the file any number of lines like import [file] and you are "importing" the contents of the files. For instance, import Mathlib.Data.Nat.Basic should work.

To get the goal appear on the left, I think that this is just a matter of dragging the windows around with VSCode (from the picture, it seems that you might be using VSCode, otherwise, I do not know). In any case, this seems more like a setup of your editor, than of Lean.

[One An]

Oh i see, thank you so much! For the goal thing, I meant like just making it appear at all because it doesn't seem to appear at all for me when I'm in tactic mode

[Damiano Testa]

What do you see if you place your cursor on the intro hp line?

[One An]

Nothing shows up

[Damiano Testa]

This is what I see

image.png

Note that the goal view is extremely sensitive to the position of the cursor: it show information about the specific place where you are. This may be nothing at all, for instance if you are between theorems.