# Zulip Chat Archive

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

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

use congr

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

:-)

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

Thanks!

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

So what does congr do?

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

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

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

that was what made me ask

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

Kevin, you should spend more time reading documentation

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

?

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

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

you win

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

:-)

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

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

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`

?

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

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

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

right

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

you'd need to generalize

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

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

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

as what?

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

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

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

I couldn't find your paper

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

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

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

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

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