Zulip Chat Archive

Stream: general

Topic: dependent congr_arg?


view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:00):

I am assuming this is provable: example (f : ℕ → ℕ) (g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type) : P f H2 = P g (H1 ▸ H2) := sorry

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:01):

The goal is P f H2 = P g _, and we have H1 : f = g

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:01):

but I can't rewrite

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:01):

because H2 is a proof of something involving f

view this post on Zulip Simon Hudon (Apr 23 2018 at 16:02):

Have you tried congr?

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:02):

I would have to rewrite f and H2 simultaneously.

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:02):

use congr

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:02):

:-)

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:02):

Thanks!

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:02):

So what does congr do?

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:02):

By which I mean

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:02):

how would I do this in term mode

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:03):

simp should also work here

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:03):

I thought I tried it and it failed

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:03):

simp doesn't work

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:03):

that was what made me ask

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:03):

Kevin, you should spend more time reading documentation

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:04):

?

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:04):

example (f : ℕ → ℕ) (g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type) : P f H2 = P g (H1 ▸ H2) := by cc

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:04):

you win

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:04):

:-)

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:04):

https://github.com/leanprover/mathlib/pull/114

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:04):

Yes, I saw it, and I even read Gabriel's explanation of what cc did

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:04):

Oh, Gabriel wrote some comment

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:04):

But the bottom line is that I still don't know what's going on

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:05):

all I know is that I'm relieved to find that I'm trying to prove something which is true

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:05):

Some months ago I would just have been happy to accept the magic

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:05):

but now I am more interested in knowing how the magic works

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:06):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
(H1  λ _, rfl :  h, P f H2 = P g h) _

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:06):

For example I don't see how to use congr_arg or congr_fun

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:06):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
eq.drec_on H1 rfl

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:06):

Thanks Kenny

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:06):

I was about to say "how do you prove this from eq.rec

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:06):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
by subst H1

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:06):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
by simp [H1]

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:06):

what is this subst?

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:07):

tactic

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:07):

takes hypothesis of the form [expr] = h or h = [expr]

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:07):

where h is any variable

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:07):

and discharge the hypothesis while substituting everything

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:07):

I like the subst proof best, in some sense, because it is closest to how I am thinking about what needs to be done

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:07):

@Mario Carneiro I now realise that simp by itself had no chance of working :-)

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:09):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
by subst H1

#print test

/-
theorem test : ∀ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type), P f H2 = P g _ :=
λ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type),
  eq.drec (eq.refl (P f H2)) H1
-/

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:10):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
eq.drec rfl H1

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:10):

should be the shortest term mode solution

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:11):

The subst proof only works because one side is a variable here, but it is able to avoid the DTT problems that many other tactics have to face in this situation

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:12):

theorem test :  (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type), P f H2 = P g (H1  H2)
| _ _ rfl _ _ := rfl

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:12):

what is so funny about that

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:12):

simp and congr both work by using congruence lemmas. These are generated on the fly and the term for them is a bit complicated but the structure is similar: from a = b and c = d derive f a c = f a b.

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:13):

The real power is that the generated congruence lemma automatically makes use of subsingletons to avoid hypotheses, meaning that if c and d are proofs then you only have one hypothesis there

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:14):

the rfl proof there is the term mode equivalent of by subst

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:14):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
by cases H1; refl

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:15):

the rfl proof there is the term mode equivalent of by subst

depends on what you mean by equivalent

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:16):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
(H1  λ _, rfl :  h, P f H2 = P g h) _

This one is my favourite :-)

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:16):

and subst is basically the same as cases or induction on an equality (although it does additional equality specific stuff like symmetry)

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:16):

Oh I just saw the | one :-)

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:16):

I think the rfl proof is equivalent to by cases

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:16):

and the by subst one is equivalent to eq.drec

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:16):

(because eq.drec is the proof generated by by subst)

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:17):

(and the | rfl one is really invoking the inductive type and equality between constructors

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:17):

like I said, they are all the same

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:17):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
by cases H1; refl

#print test

/-
theorem test : ∀ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type), P f H2 = P g _ :=
λ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type),
  eq.dcases_on H1
    (λ (H_1 : g = f), eq.rec (λ (H1 : f = f) (H_2 : H1 == eq.refl f), eq.refl (P f H2)) (eq.symm H_1) H1)
    (eq.refl g)
    (heq.refl H1)
-/

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:17):

theorem test :  (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type), P f H2 = P g (H1  H2)
| _ _ rfl _ _ := rfl

#print test

/-
theorem test : ∀ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type), P f H2 = P g _ :=
λ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type),
  eq.dcases_on H1
    (λ (H_1 : g = f), eq.rec (λ (H1 : f = f) (H_2 : H1 == eq.refl f), id_rhs (P f H2 = P f H2) rfl) (eq.symm H_1) H1)
    (eq.refl g)
    (heq.refl H1)
-/

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:17):

they're exactly the same

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:18):

eq.dcases_on is the same as eq.drec I believe

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:18):

no there's an id_rhs` in one but not the other

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:19):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
eq.dcases_on H1 rfl

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:19):

I think you would get the exact same term if you use by refl instead of rfl in the term proof

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:19):

no there's an id_rhs` in one but not the other

aha

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:19):

I like the | proof because it is a really powerful way of doing the substitution.

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:20):

the term mode equivalent is cases

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:20):

If you replace f and g by constants this proof won't work

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:21):

right

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:21):

you'd need to generalize

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:21):

or simp

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:22):

simp uses congr, so it can do dependent rewrite

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:22):

theorem test (f :   ) (g :   ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h :   ), h 0 = 0  Type) : P f H2 = P g (H1  H2) :=
by congr; from H1

#print test

/-
theorem test : ∀ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type), P f H2 = P g _ :=
λ (f g : ℕ → ℕ) (H1 : f = g) (H2 : f 0 = 0) (P : Π (h : ℕ → ℕ), h 0 = 0 → Type),
  (λ (h h_1 : ℕ → ℕ) (e_1 : h = h_1) (a : h 0 = 0) (a_1 : h_1 0 = 0),
     (λ (h h_1 : ℕ → ℕ) (e_1 : h = h_1) (a : h 0 = 0), eq.drec (eq.refl (P h (eq.rec a (eq.refl h)))) e_1) h h_1
       e_1
       a)
    f
    g
    H1
    H2
    (H1 ▸ H2)
-/

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:23):

I think that's the same proof term after some beta reduction

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:23):

as what?

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:23):

the last few

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:23):

every proof is equal because of proof irrelevance

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:23):

Well, modulo #reduce reduction I think all proofs so far are the same

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:25):

church rosser much

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:25):

did you check out my paper? C-R is false in lean

view this post on Zulip Kenny Lau (Apr 23 2018 at 16:26):

I couldn't find your paper

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:49):

Kenny: https://github.com/digama0/lean-type-theory/releases/

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:49):

and the reason I'm reviving this thread is that I discovered that in my use case, not all of the solutions worked.

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:50):

my actual goal is extend_map_of_im_unit (g ∘ of_comm_ring R S) _ = extend_map_of_im_unit (of_comm_ring R S) H where of_comm_ring R S is a ring homomorphism, so quite a bit more structurally complicated than my toy MWE

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:51):

and congr gave me three random goals, one of which was loc R S = (R × ↥S) and that might not even be true.

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:51):

cc also didn't work

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:52):

but Kenny's eq.drec_on H1 rfl worked.

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:52):

simp didn't work

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:53):

both subst and simp complained that H1 wasn't an appropriate lemma

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:53):

even though it was of the form X = Y

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 20:54):

I realise now that I am using tactics less and less, I am on the whole doing quite abstract maths and the arguments are in some sense straightforward to show from first principles, so I don't really need any tactics beyond rw.

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 21:11):

aargh actually none of them worked :-/ the eq.drec approach looks like it works, but an error appears elsewhere. cases H1 gave me an error I'd never seen before :-)

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 21:11):

cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
(λ (x : R), g (of_comm_ring R S x)) = λ (r : R), ⟦(r, ⟨1, _⟩)⟧

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 21:12):

that's surprising because H1 is of_comm_ring R S = g ∘ of_comm_ring R S.

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 21:13):

I don't need this lemma, I might give up on it.


Last updated: May 08 2021 at 10:12 UTC