introducing variables

Stream: new members

[Ali Sever]

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.

[Mario Carneiro]

mathlib has rcases for this

[Mario Carneiro]

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

[Mario Carneiro]

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

[Ali Sever]

Is there a similar thing for term mode?

[Mario Carneiro]

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

[Ali Sever]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Ali Sever]

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'.

[Ali Sever]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

wow that's a nice project page

[Patrick Massot]

Yes, mathlib could use a webdesigner

[Ali Sever]

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.

[Patrick Massot]

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