My first original result

Stream: new members

[Jeremy Teitelbaum]

My first original result proved in Lean.

example : 0 \in (2 :: 1 :: 0 :: list.nil) :=
begin
   right,
   right,
   left,
  refl,
end

[Martin Dvořák]

Welcome!

[Adam Topaz]

Can you get the proof to a single line?

[Adam Topaz]

Hint: the computer can compute whether or not a given natural is in a list of naturals ;)

[Jeremy Teitelbaum]

What I'd really like to understand is how to write this without tactics. Or, more generally, I confess I don't exactly understand what right and left are doing, from the internal point of view. I gather that they apply the first and second constructors of an inductive type. But what is the inductive type under consideration here? I'm trying to read the source code for the list type but I can't match things up.

[Marcus Rossel]

Jeremy Teitelbaum said:

What I'd really like to understand is how to write this without tactics. Or, more generally, I confess I don't exactly understand what right and left are doing, from the internal point of view. I gather that they apply the first and second constructors of an inductive type. But what is the inductive type under consideration here? I'm trying to read the source code for the list type but I can't match things up.

You can use the #print command to inspect the term that was constructed by a begin-end block:

theorem my_theorem : 0 ∈ (2 :: 1 :: 0 :: list.nil) :=
begin
   right,
   right,
   left,
  refl,
end

#print my_theorem
--theorem my_theorem : 0 ∈ [2, 1, 0] :=  or.inr (or.inr (or.inl (eq.refl 0)))

[Adam Topaz]

left and right are tactics that you can use when you want to prove a disjunction of two props $p \vee q$. If the goal is $p \vee q$, then left will replace the goal with $p$ and right will replace the goal with $q$.

[Adam Topaz]

The has_mem instance for a list is defined recursively so that $x \in (a :: as)$ if and only if $x = a$ or $x \in as$, and this is why left and/or right work for such a goal.

[Adam Topaz]

(the base case x \in list.nil is defined to be false.)

[Patrick Massot]

Jeremy, do you know about tactic#show_term?

[Jeremy Teitelbaum]

The process by which 0 \in [0,1,2] gets converted to 0=0 \or 0\in [1,2] seems like utter magic.

[Marcus Rossel]

Jeremy Teitelbaum said:

The process by which 0 \in [0,1,2] gets converted to 0=0 \or 0\in [1,2] seems like utter magic.

That comes from the definition of list.mem:

protected def mem : α → list α → Prop
| a []       := false
| a (b :: l) := a = b ∨ mem a l

From this definition we can deduce that 0 \in [0,1,2] (which is syntactic sugar for list.mem 0 [0, 1, 2]) means the same as 0 = 0 ∨ list.mem 0 [1, 2].

[Kevin Buzzard]

Jeremy, there is this weird non-mathematical concept called definitional equality.

[Kevin Buzzard]

For example x+0=x is definitionally true, but 0+x=x is not, you need to prove it by induction.

[Jeremy Teitelbaum]

Yes, I see that. But I can't find this syntax for definition of a function in the manual. (probably just dumb). I can infer its meaning, but what language mechanism takes a statement like list.mem 0 [0,1,2], which I gather is a proposition, and rewrites it as the appropriate \or taking into account that [0,1,2] is not null?

[Kevin Buzzard]

You don't need manuals, you just right click on what you want to see the definition of

[Kevin Buzzard]

#check list.mem, right click, see what the definitional equalities are

[Kevin Buzzard]

or unfold list.mem in tactic mode

[Marcus Rossel]

Jeremy Teitelbaum said:

Yes, I see that. But I can't find this syntax for definition of a function in the manual. (probably just dumb). I can infer its meaning, but what language mechanism takes a statement like list.mem 0 [0,1,2], which I gather is a proposition, and rewrites it as the appropriate \or taking into account that [0,1,2] is not null?

For the syntax, cf. https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching

[Jeremy Teitelbaum]

Marcus Rossel said:

For the syntax, cf. https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching

Aha. I am still trying to make sense of the discussion of inductive types in chapter 7. I will press on. Thanks!

[Kevin Buzzard]

The definition of list.memsays that a \in [] is defined to be false and a \in b :: l is defined to be a = b \or a \in l

[Patrick Johnson]

Jeremy Teitelbaum said:

What I'd really like to understand is how to write this without tactics.

lemma lem : 0 ∈ [2, 1, 0] := of_as_true trivial

[Kevin Buzzard]

you just keep unwinding the definitions and at each point you observe that there is an algorithm to determine whether the proposition is true or not, so you just keep applying the algorithm.

[Kevin Buzzard]

equality is decidable for concrete naturals, and if P and Q are decidable then P or Q is decidable (because you just decide them both and see if either are true)