## Stream: maths

### Topic: cases in term mode

#### 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


#### Mario Carneiro (May 01 2018 at 09:42):

hint: use list.chain

#### 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)


interesting

#### 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?

#### 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

#### 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)


#### Johan Commelin (May 01 2018 at 09:47):

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

#### Mario Carneiro (May 01 2018 at 09:47):

you could use list.chain for the latter two cases

#### Kenny Lau (May 01 2018 at 09:47):

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

#### Mario Carneiro (May 01 2018 at 09:48):

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

#### Kenny Lau (May 01 2018 at 09:48):

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

not for this...

#### 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

#### Mario Carneiro (May 01 2018 at 09:49):

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

oh what

#### Johan Commelin (May 01 2018 at 09:51):

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

#### Kenny Lau (May 01 2018 at 09:52):

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

#### Kenny Lau (May 01 2018 at 09:52):

not to confuse you

#### Johan Commelin (May 01 2018 at 09:53):

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

#### Kenny Lau (May 01 2018 at 09:53):

yours? I haven't seen your definition

#### Johan Commelin (May 01 2018 at 09:54):

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

#### Kenny Lau (May 01 2018 at 09:54):

but I haven't finished my second definition

Aaah, ok

#### 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?

#### 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

#### Kenny Lau (May 01 2018 at 09:57):

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

#### Mario Carneiro (May 01 2018 at 09:57):

you probably need induction-recursion-recursion or something

#### Kenny Lau (May 01 2018 at 09:57):

hmm

Last updated: May 12 2021 at 06:14 UTC