Zulip Chat Archive

Stream: new members

Topic: Rewriting in assumption


view this post on Zulip Mukesh Tiwari (May 09 2020 at 01:42):

I want to prove this lemma, where F is a Field.

lemma eqor :  (y₁ y₂ : F),
   (y₁ - y₂) * (y₁ + y₂) = 0  y₁ = y₂  y₁ = -y₂ :=
   begin
    intros,
    /- I want to multiply (y₁ + y₂)⁻¹ in a
       to y₁ = y₂ -/

   end

and my goal is:

state:
F : Type u_2,
_inst_2 : decidable_eq F,
_inst_4 : field F,
y₁ y₂ : F,
a : (y₁ - y₂) * (y₁ + y₂) = 0
 y₁ = y₂  y₁ = -y₂

What I want is to multiply (y₁ + y₂)⁻¹ in a to infer (y₁ - y₂) = 0, and similarly, (y₁ + y₂) = 0. How can I do this ?

view this post on Zulip Alex J. Best (May 09 2020 at 01:49):

lemma eqor {F: Type*} [field F] :  (y₁ y₂ : F),
   (y₁ - y₂) * (y₁ + y₂) = 0  y₁ = y₂  y₁ = -y₂ :=
   begin
    intros,
    classical,
    by_cases h : y₁ - y₂ = 0,
    {
      sorry,
    },
    {
      apply_fun ((*) (y₁ - y₂)⁻¹) at a,
      rw [mul_zero,  mul_assoc, inv_mul_cancel h, one_mul] at a,
      sorry,
    }
   end

view this post on Zulip Jalex Stark (May 09 2020 at 01:50):

I guess to make this a #mwe you need to add

variables {F : Type}
variables [field F]
variables [decidable_eq F]

?

view this post on Zulip Jalex Stark (May 09 2020 at 01:51):

Alex, that looks right to me? why did you delete it?

view this post on Zulip Alex J. Best (May 09 2020 at 01:51):

It was in the wrong order, rewriting

view this post on Zulip Mukesh Tiwari (May 09 2020 at 01:52):

I deleted nothing, but it was re-formatting (but let me add all the information).

view this post on Zulip Alex J. Best (May 09 2020 at 01:52):

Maybe there is a way to avoid by cases, but this should work

view this post on Zulip Mukesh Tiwari (May 09 2020 at 01:56):

I am getting unknown identifier for 'apply_fun'.

view this post on Zulip Mukesh Tiwari (May 09 2020 at 01:57):

Here is my complete source code (if that helps): https://gist.github.com/mukeshtiwari/23a6256f4edd109f6fe820704bc6aa9c

view this post on Zulip Jalex Stark (May 09 2020 at 01:57):

Alex should add import tactic to the beginning of their example

view this post on Zulip Jalex Stark (May 09 2020 at 01:58):

Mukesh, instead of linking your whole source code, you should make a #mwe

view this post on Zulip Jalex Stark (May 09 2020 at 01:58):

(if you click on the link, the community definition of mwe will appear)

view this post on Zulip Bryan Gin-ge Chen (May 09 2020 at 01:59):

Here's another proof:

import algebra.field

variables (F : Type*) [field F] -- [decidable_eq F]

lemma eqor :  (y₁ y₂ : F),
   (y₁ - y₂) * (y₁ + y₂) = 0  y₁ = y₂  y₁ = -y₂ :=
   begin
    intros,
    rw mul_eq_zero at a,
    cases a,
    { left, rwa [sub_eq_zero] at a, },
    { right, rwa [add_eq_zero_iff_eq_neg] at a, },
    /- I want to multiply (y₁ + y₂)⁻¹ in a
       to y₁ = y₂ -/
   end

view this post on Zulip Jalex Stark (May 09 2020 at 02:02):

Bryan's proof is nicer, but I guess the answer to Mukesh's original question is apply_fun

view this post on Zulip Jalex Stark (May 09 2020 at 02:02):

@Mukesh Tiwari , apply_fun is provided by import tactic or if you want to be conservative, import tactic.apply_fun

view this post on Zulip Mukesh Tiwari (May 09 2020 at 02:03):

Thank you very much every one. I wanted to know how apply (or rewrite in a hypothesis). In Coq, I can simply apply f in H or rewrite H1 in H2. So, both answers are very helpful.

view this post on Zulip Bryan Gin-ge Chen (May 09 2020 at 02:04):

Yeah, for some reason, the preposition we use in lean is at, not in.

view this post on Zulip Jalex Stark (May 09 2020 at 02:06):

If you run through the natural number game, you'd probably pick up several of these "Coq translations" pretty quickly

view this post on Zulip Jalex Stark (May 09 2020 at 02:06):

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/


Last updated: May 08 2021 at 10:12 UTC