Zulip Chat Archive

Stream: new members

Topic: introducing variables


view this post on Zulip Ali Sever (Jul 19 2018 at 21:06):

If I have a Prop that says ∃ a b c, p, whats the quickest way of introducing a b c and p? In tactic mode, I have to use cases three times to obtain all of them.

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:09):

mathlib has rcases for this

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:09):

rcases h with ⟨a, b, c, hp⟩

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:10):

there is also rintro for introducing and casing at the same time, rintro ⟨a, b, c, hp⟩ takes a goal of the form (∃ a b c, p) -> q and splits off the parts and has q as subgoal

view this post on Zulip Ali Sever (Jul 19 2018 at 21:12):

Is there a similar thing for term mode?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:13):

let ⟨a, b, c, hp⟩ := h in ... is the equivalent of rcases and λ ⟨a, b, c, hp⟩, is the equivalent of rintro. Neither of those require mathlib

view this post on Zulip Ali Sever (Jul 21 2018 at 10:32):

I have def col (a b c : point) : Prop := B a b c ∨ B b c a ∨ B c a b. I want to prove col a b c ∧ (some other stuff) → col a' b' c'. Depending on the cases of col a b c, all the proofs are the same. So can I name {a, b, c} = {x, y, z} such that B x y z is true. So that when I prove B x' y' z', I will have proven col a' b' c'?

view this post on Zulip Mario Carneiro (Jul 21 2018 at 10:34):

what is the relation between x',y',z' and a',b',c'?

view this post on Zulip Mario Carneiro (Jul 21 2018 at 10:37):

One option is to prove as a lemma/have something like \forall x y z, B x y z ∧ (some other stuff) → B x' y' z' (where presumably x' is a function of x or something), and then instantiate it three times for the final proof

view this post on Zulip Ali Sever (Jul 21 2018 at 10:37):

I can prove B a b c → B a' b' c' for any order of a,b and c. So if x = a, x' = a'.

view this post on Zulip Ali Sever (Jul 21 2018 at 10:38):

Ah, and then when I do cases, I can just use lemma _ _ _ and let lean guess the order.

view this post on Zulip Mario Carneiro (Jul 21 2018 at 10:39):

Depending on how often you need this, it might even be worth making a lemma to abstract this proof pattern

view this post on Zulip Mario Carneiro (Jul 21 2018 at 10:40):

By the way, from your two questions I have a pretty good idea what you are working on ;)

view this post on Zulip Patrick Massot (Jul 21 2018 at 11:20):

@Ali Sever Are you aware of http://geocoq.github.io/GeoCoq/?

view this post on Zulip Mario Carneiro (Jul 21 2018 at 11:20):

wow that's a nice project page

view this post on Zulip Patrick Massot (Jul 21 2018 at 11:25):

Yes, mathlib could use a webdesigner

view this post on Zulip Ali Sever (Jul 21 2018 at 11:27):

Yes, I looked around and I found out they were using the same book I was. I don't know exactly how Coq works, but when I get better at lean, I hope to write some interesting tactics.

view this post on Zulip Patrick Massot (Jul 21 2018 at 11:28):

But the message for Ali was rather more: beware that formalizing elementary geometry can be a lifetime project, especially because of the kind of symmetry issues that appeared in your question. See in particular https://hal.inria.fr/hal-00989781v2


Last updated: May 08 2021 at 09:11 UTC