cases in term mode

Stream: maths

[Johan Commelin]

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]

hint: use list.chain

[Kenny Lau]

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)

[Kenny Lau]

interesting

[Johan Commelin]

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

[Mario Carneiro]

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

[Kenny Lau]

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]

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

[Mario Carneiro]

you could use list.chain for the latter two cases

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

not for this...

[Kenny Lau]

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]

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

[Kenny Lau]

oh what

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

not to confuse you

[Johan Commelin]

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

[Kenny Lau]

yours? I haven't seen your definition

[Johan Commelin]

Hmm, agreed. My bad.

[Johan Commelin]

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

[Kenny Lau]

but I haven't finished my second definition

[Johan Commelin]

Aaah, ok

[Kenny Lau]

@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]

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]

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

[Mario Carneiro]

you probably need induction-recursion-recursion or something

[Kenny Lau]

hmm