Zulip Chat Archive

Stream: maths

Topic: cases in term mode


view this post on Zulip Johan Commelin (May 01 2018 at 09:40):

I am trying to tell Lean what a path in a quiver is. How do I finish is_a_path?

universes u

structure quiver :=
(V : Type u)
(E : Type u)
(s : E  V)
(t : E  V)

variable {Q : quiver}

definition is_a_path : (list Q.E)  Prop :=
λ l, sorry

view this post on Zulip Mario Carneiro (May 01 2018 at 09:42):

hint: use list.chain

view this post on Zulip Kenny Lau (May 01 2018 at 09:43):

inductive list.chain : Π {α : Type u}, (α  α  Prop)  α  list α  Prop
constructors:
list.chain.nil :  {α : Type u} (R : α  α  Prop) (a : α), list.chain R a list.nil
list.chain.cons :  {α : Type u} {R : α  α  Prop} {a b : α} {l : list α},
  R a b  list.chain R b l  list.chain R a (b :: l)

view this post on Zulip Kenny Lau (May 01 2018 at 09:43):

interesting

view this post on Zulip Johan Commelin (May 01 2018 at 09:44):

By the way, do you think it is a good idea to use lists to capture paths?

view this post on Zulip Mario Carneiro (May 01 2018 at 09:46):

You may want more complicated inductive structures in some circumstances, but here a list of edges is sufficient

view this post on Zulip Kenny Lau (May 01 2018 at 09:46):

universes u v

structure quiver :=
(V : Type u)
(E : Type v)
(s : E  V)
(t : E  V)

variable {Q : quiver}

definition is_a_path : (list Q.E)  Prop
| []             := true
| [x]            := true
| (hd1::hd2::tl) := Q.t hd1 = Q.s hd2  is_a_path (hd2::tl)

view this post on Zulip Johan Commelin (May 01 2018 at 09:47):

Aaah, so I should use |. Thanks! But now you are not using list.chain

view this post on Zulip Mario Carneiro (May 01 2018 at 09:47):

you could use list.chain for the latter two cases

view this post on Zulip Kenny Lau (May 01 2018 at 09:47):

the definition using list.chain is left to the reader as an exercise :P

view this post on Zulip Mario Carneiro (May 01 2018 at 09:48):

alternatively, you could define it as an inductive type, which may be more natural

view this post on Zulip Kenny Lau (May 01 2018 at 09:48):

oh... I just realized I wanted induction-recursion

view this post on Zulip Mario Carneiro (May 01 2018 at 09:48):

not for this...

view this post on Zulip Kenny Lau (May 01 2018 at 09:49):

mutual inductive path, head
with path : Type (max u v)
| A : Q.E  path
with head : path  Q.V
| (path.A x) := _

failed idea

view this post on Zulip Mario Carneiro (May 01 2018 at 09:49):

you want the head to be a parameter, like in chain

view this post on Zulip Kenny Lau (May 01 2018 at 09:50):

oh what

view this post on Zulip Johan Commelin (May 01 2018 at 09:51):

Kenny, I don't understand your last definition. What does mutual do?

view this post on Zulip Kenny Lau (May 01 2018 at 09:51):

https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf
P.120, Section 7.9

view this post on Zulip Kenny Lau (May 01 2018 at 09:52):

note that I was trying induction-recursion which is not a thing

view this post on Zulip Kenny Lau (May 01 2018 at 09:52):

not to confuse you

view this post on Zulip Johan Commelin (May 01 2018 at 09:53):

But your current definition is not equivalent to mine, right?

view this post on Zulip Kenny Lau (May 01 2018 at 09:53):

yours? I haven't seen your definition

view this post on Zulip Johan Commelin (May 01 2018 at 09:54):

Hmm, agreed. My bad.

view this post on Zulip Johan Commelin (May 01 2018 at 09:54):

Let me try again: your second definition is not equivalent to your first, right?

view this post on Zulip Kenny Lau (May 01 2018 at 09:54):

but I haven't finished my second definition

view this post on Zulip Johan Commelin (May 01 2018 at 09:55):

Aaah, ok

view this post on Zulip Kenny Lau (May 01 2018 at 09:55):

@Mario Carneiro (maybe on its own thread?) if Lean had induction-recursion, would you be able to prove false? would there be a shorter proof than following godel?

view this post on Zulip Mario Carneiro (May 01 2018 at 09:56):

No. Induction recursion would strengthen the system, it wouldn't be able to prove its own consistency because it now has induction-recursion and the simulated lean language would not

view this post on Zulip Kenny Lau (May 01 2018 at 09:57):

why can't you simulate induction-recursion with induction-recursion?

view this post on Zulip Mario Carneiro (May 01 2018 at 09:57):

you probably need induction-recursion-recursion or something

view this post on Zulip Kenny Lau (May 01 2018 at 09:57):

hmm


Last updated: May 12 2021 at 06:14 UTC