Zulip Chat Archive

Stream: new members

Topic: applying definitions to theorems


Danila Kurganov (Feb 28 2020 at 16:02):

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 (Feb 28 2020 at 16:03):

Try unfold equivalency at *

Danila Kurganov (Feb 28 2020 at 16:06):

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 (Feb 28 2020 at 16:13):

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

Danila Kurganov (Feb 28 2020 at 16:16):

That's a neat site, thanks.

Bryan Gin-ge Chen (Feb 28 2020 at 16:21):

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 (Feb 28 2020 at 16:45):

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 (Feb 28 2020 at 16:50):

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 (Feb 28 2020 at 17:22):

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

Kevin Buzzard (Feb 28 2020 at 17:22):

he means your next move after unfold

Kevin Buzzard (Feb 28 2020 at 17:23):

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

Danila Kurganov (Feb 28 2020 at 17:32):

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

Danila Kurganov (Feb 28 2020 at 18:01):

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 (Feb 28 2020 at 18:02):

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

Kevin Buzzard (Feb 28 2020 at 18:03):

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

Kevin Buzzard (Feb 28 2020 at 18:06):

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

Your definition is not what you think it is.

Kevin Buzzard (Feb 28 2020 at 18:06):

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 (Mar 03 2020 at 16:35):

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 (Mar 03 2020 at 16:36):

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

Kevin Buzzard (Mar 03 2020 at 16:39):

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 (Mar 03 2020 at 16:48):

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

Kevin Buzzard (Mar 03 2020 at 16:49):

No, it switches Lean into maths mode.

Danila Kurganov (Mar 03 2020 at 16:50):

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

Kevin Buzzard (Mar 03 2020 at 16:52):

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 (Mar 03 2020 at 16:57):

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 (Mar 03 2020 at 16:59):

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


Last updated: Dec 20 2023 at 11:08 UTC