applying definitions to theorems

Stream: new members

[Danila Kurganov]

Hi, I'm having trouble trying to use my own definitions and applying them to theorems,
how should I approach the following if I wanted to unpack my definition once lean knows there's a proof of it?

def equivalency (p q : Prop) : Prop := p → q ∧ q → p

theorem (p q : Prop) : equivalency p q → p ∧ q :=
begin
  intro eq_pq,
  -- how do I unpack my definition now?
end

Thanks!

[Donald Sebastian Leung]

Try unfold equivalency at *

[Danila Kurganov]

Thanks, that works perfectly- If I wanted to find out more about the unfold tactic (source code maybe?) where should I go? I've not found the tactic codes so far..

[Kevin Buzzard]

There are lots of tactics, and I picked up the ones which were useful for me by just asking lots of questions.

[Danila Kurganov]

That's a neat site, thanks.

[Bryan Gin-ge Chen]

The doc page that Kevin linked to mostly discusses tactics in mathlib. The source code for those tactics can be found in the src/tactic directory of mathlib. The unfold tactic is provided in the core library and its source code is here. It relies on much of the same code as the very important simp tactic, which you can read more about here.

[Danila Kurganov]

Will have a read- and I forgot to check src! good to know it's all there. Didn't know simp was much more intricate under-the-hood, good to know

[Reid Barton]

Some tactics (like cases/rcases which is probably coming next) will automatically see through definitional equalities, making unfold redundant once you know what the next step should be.

[Danila Kurganov]

By 'which is probably coming next' you mean some new version of Lean?

[Kevin Buzzard]

he means your next move after unfold

[Kevin Buzzard]

Isn't your theorem false by the way? p and q could both be false right?

[Danila Kurganov]

Oh got it; and yeah it's quite false, I've changed it to including that case too

[Danila Kurganov]

it does seem like I am still in a bit of a pickle by the way- I want to use the fact that if one's not true the other must be true; (so I've tried using by_cases), yet my expression is 'not decidable'.. any thoughts?

theorem (p q: Prop) : equivalency p q → ((p ∧ q) ∨ ((¬ p) ∧ (¬ q))) :=
begin
  intro eq,
  unfold equivalency at *,
  cases eq with pq qp,
  --by_cases h : p ∧ q,
end

I sort of want to just do the casework and/or use a contradiction

[Kevin Buzzard]

Your code doesn't work at all for me. Can you post something which compiles?

[Kevin Buzzard]

Oh -- does the cases line not work for you either?

[Kevin Buzzard]

def equivalency (p q : Prop) : Prop := (p → q) ∧ (q → p)

Your definition is not what you think it is.

[Kevin Buzzard]

import tactic

def equivalency (p q : Prop) : Prop := (p → q) ∧ (q → p)

open_locale classical

theorem x (p q: Prop) : equivalency p q → ((p ∧ q) ∨ ((¬ p) ∧ (¬ q))) :=
begin
  intro eq,
  unfold equivalency at eq,
  cases eq,
  by_cases hp : p; by_cases hq : q,
    finish,
    finish,
    finish,
    finish,
end

[Danila Kurganov]

I never would have known that I have defined my equivalency poorly; I think it sort of doesn't 'say' anything; but now the by_cases tactic makes much more sense

[Danila Kurganov]

What does this open_locale classical do? It got rid of many red underlines in my vs code

[Kevin Buzzard]

It means that you can assume that every true/false statement is either true or false. Some tactics like finish assume this. Some computer scientists don't like assuming this shrug

[Danila Kurganov]

So it just tells Lean what it can assume for the time being, got it thanks

[Kevin Buzzard]

No, it switches Lean into maths mode.

[Danila Kurganov]

By maths mode you mean propositions are either true or false.. or is there something more to this?

[Kevin Buzzard]

I mean that you can assume many things such as the law of the excluded middle, decidability of all propositions etc, things which mathematicians assume all the time without ever questioning that it could be any other way, but some computer scientists don't like to assume because they might want their code to be "constructive", which is some technical thing we don't teach in the maths department.

[Danila Kurganov]

I quite like how it can be constructive, but for the time being I'm guessing typing open_locale classical should just be a habit then for usual maths. Thanks

[Reid Barton]

In this case you need classical reasoning for x (equivalency p p is true, and then you conclude p or not p.)