Zulip Chat Archive

Stream: new members

Topic: My first original result


Jeremy Teitelbaum (Dec 22 2021 at 15:47):

My first original result proved in Lean.

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

Martin Dvořák (Dec 22 2021 at 15:57):

Welcome!

Adam Topaz (Dec 22 2021 at 16:18):

Can you get the proof to a single line?

Adam Topaz (Dec 22 2021 at 16:18):

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

Jeremy Teitelbaum (Dec 22 2021 at 16:42):

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 (Dec 22 2021 at 16:44):

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 (Dec 22 2021 at 16:44):

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

Adam Topaz (Dec 22 2021 at 16:45):

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

Adam Topaz (Dec 22 2021 at 16:45):

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

Patrick Massot (Dec 22 2021 at 16:47):

Jeremy, do you know about tactic#show_term?

Jeremy Teitelbaum (Dec 22 2021 at 16:47):

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 (Dec 22 2021 at 16:48):

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 (Dec 22 2021 at 16:50):

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

Kevin Buzzard (Dec 22 2021 at 16:50):

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

Jeremy Teitelbaum (Dec 22 2021 at 16:50):

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 (Dec 22 2021 at 16:51):

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

Kevin Buzzard (Dec 22 2021 at 16:52):

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

Kevin Buzzard (Dec 22 2021 at 16:52):

or unfold list.mem in tactic mode

Marcus Rossel (Dec 22 2021 at 16:52):

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 (Dec 22 2021 at 16:54):

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 (Dec 22 2021 at 16:58):

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 (Dec 22 2021 at 17:00):

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 (Dec 22 2021 at 17:01):

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 (Dec 22 2021 at 17:01):

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)


Last updated: Dec 20 2023 at 11:08 UTC