## Stream: general

### Topic: dependent congr_arg?

#### 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

#### Kevin Buzzard (Apr 23 2018 at 16:01):

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

#### Kevin Buzzard (Apr 23 2018 at 16:01):

but I can't rewrite

#### Kevin Buzzard (Apr 23 2018 at 16:01):

because H2 is a proof of something involving f

#### Simon Hudon (Apr 23 2018 at 16:02):

Have you tried congr?

#### Kevin Buzzard (Apr 23 2018 at 16:02):

I would have to rewrite f and H2 simultaneously.

use congr

:-)

Thanks!

#### Kevin Buzzard (Apr 23 2018 at 16:02):

So what does congr do?

By which I mean

#### Kevin Buzzard (Apr 23 2018 at 16:02):

how would I do this in term mode

#### Mario Carneiro (Apr 23 2018 at 16:03):

simp should also work here

#### Kevin Buzzard (Apr 23 2018 at 16:03):

I thought I tried it and it failed

#### Kevin Buzzard (Apr 23 2018 at 16:03):

simp doesn't work

#### Patrick Massot (Apr 23 2018 at 16:03):

Kevin, you should spend more time reading documentation

?

#### 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

you win

:-)

#### Patrick Massot (Apr 23 2018 at 16:04):

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

#### Kevin Buzzard (Apr 23 2018 at 16:04):

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

#### Patrick Massot (Apr 23 2018 at 16:04):

Oh, Gabriel wrote some comment

#### Kevin Buzzard (Apr 23 2018 at 16:04):

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

#### 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

#### Kevin Buzzard (Apr 23 2018 at 16:05):

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

#### Kevin Buzzard (Apr 23 2018 at 16:05):

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

#### 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) _


#### Kevin Buzzard (Apr 23 2018 at 16:06):

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

#### 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


Thanks Kenny

#### Kevin Buzzard (Apr 23 2018 at 16:06):

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

#### 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


#### 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]


#### Kevin Buzzard (Apr 23 2018 at 16:06):

what is this subst?

tactic

#### Kenny Lau (Apr 23 2018 at 16:07):

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

#### Kenny Lau (Apr 23 2018 at 16:07):

where h is any variable

#### Kenny Lau (Apr 23 2018 at 16:07):

and discharge the hypothesis while substituting everything

#### 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

#### Kevin Buzzard (Apr 23 2018 at 16:07):

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

#### 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
-/


#### 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


#### Kenny Lau (Apr 23 2018 at 16:10):

should be the shortest term mode solution

#### 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

#### 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


#### Kenny Lau (Apr 23 2018 at 16:12):

what is so funny about that

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

#### 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

#### Mario Carneiro (Apr 23 2018 at 16:14):

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

#### 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


#### 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

#### 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 :-)

#### 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)

#### Kevin Buzzard (Apr 23 2018 at 16:16):

Oh I just saw the | one :-)

#### Kenny Lau (Apr 23 2018 at 16:16):

I think the rfl proof is equivalent to by cases

#### Kenny Lau (Apr 23 2018 at 16:16):

and the by subst one is equivalent to eq.drec

#### Kenny Lau (Apr 23 2018 at 16:16):

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

#### Kenny Lau (Apr 23 2018 at 16:17):

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

#### Mario Carneiro (Apr 23 2018 at 16:17):

like I said, they are all the same

#### 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)
-/


#### 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)
-/


#### Kenny Lau (Apr 23 2018 at 16:17):

they're exactly the same

#### Mario Carneiro (Apr 23 2018 at 16:18):

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

#### Kevin Buzzard (Apr 23 2018 at 16:18):

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

#### 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


#### 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

#### Kenny Lau (Apr 23 2018 at 16:19):

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

aha

#### Kevin Buzzard (Apr 23 2018 at 16:19):

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

#### Kenny Lau (Apr 23 2018 at 16:20):

the term mode equivalent is cases

#### Mario Carneiro (Apr 23 2018 at 16:20):

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

right

#### Kenny Lau (Apr 23 2018 at 16:21):

you'd need to generalize

or simp

#### Mario Carneiro (Apr 23 2018 at 16:22):

simp uses congr, so it can do dependent rewrite

#### 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)
-/


#### Mario Carneiro (Apr 23 2018 at 16:23):

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

as what?

the last few

#### Kenny Lau (Apr 23 2018 at 16:23):

every proof is equal because of proof irrelevance

#### Mario Carneiro (Apr 23 2018 at 16:23):

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

#### Kenny Lau (Apr 23 2018 at 16:25):

church rosser much

#### Mario Carneiro (Apr 23 2018 at 16:25):

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

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

#### 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

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

#### Kevin Buzzard (Apr 23 2018 at 20:51):

cc also didn't work

#### Kevin Buzzard (Apr 23 2018 at 20:52):

but Kenny's eq.drec_on H1 rfl worked.

simp didn't work

#### Kevin Buzzard (Apr 23 2018 at 20:53):

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

#### Kevin Buzzard (Apr 23 2018 at 20:53):

even though it was of the form X = Y

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

#### 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 :-)

#### 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, _⟩)⟧


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

#### 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