dependent congr_arg?

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

but I can't rewrite

[Kevin Buzzard]

because H2 is a proof of something involving f

[Simon Hudon]

Have you tried congr?

[Kevin Buzzard]

I would have to rewrite f and H2 simultaneously.

[Mario Carneiro]

use congr

[Kevin Buzzard]

:-)

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

So what does congr do?

[Kevin Buzzard]

By which I mean

[Kevin Buzzard]

how would I do this in term mode

[Mario Carneiro]

simp should also work here

[Kevin Buzzard]

I thought I tried it and it failed

[Kevin Buzzard]

simp doesn't work

[Kevin Buzzard]

that was what made me ask

[Patrick Massot]

Kevin, you should spend more time reading documentation

[Kevin Buzzard]

?

[Patrick Massot]

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]

you win

[Kevin Buzzard]

:-)

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

Oh, Gabriel wrote some comment

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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]

Thanks Kenny

[Kevin Buzzard]

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

[Kenny Lau]

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]

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]

what is this subst?

[Kenny Lau]

tactic

[Kenny Lau]

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

[Kenny Lau]

where h is any variable

[Kenny Lau]

and discharge the hypothesis while substituting everything

[Kevin Buzzard]

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]

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

[Kenny Lau]

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]

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]

should be the shortest term mode solution

[Mario Carneiro]

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]

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]

what is so funny about that

[Mario Carneiro]

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]

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]

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

[Kenny Lau]

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]

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

depends on what you mean by equivalent

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Oh I just saw the | one :-)

[Kenny Lau]

I think the rfl proof is equivalent to by cases

[Kenny Lau]

and the by subst one is equivalent to eq.drec

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

like I said, they are all the same

[Kenny Lau]

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]

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]

they're exactly the same

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

aha

[Kevin Buzzard]

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

[Kenny Lau]

the term mode equivalent is cases

[Mario Carneiro]

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

[Kenny Lau]

right

[Kenny Lau]

you'd need to generalize

[Mario Carneiro]

or simp

[Mario Carneiro]

simp uses congr, so it can do dependent rewrite

[Kenny Lau]

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]

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

[Kenny Lau]

as what?

[Mario Carneiro]

the last few

[Kenny Lau]

every proof is equal because of proof irrelevance

[Mario Carneiro]

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

[Kenny Lau]

church rosser much

[Mario Carneiro]

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

[Kenny Lau]

I couldn't find your paper

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

cc also didn't work

[Kevin Buzzard]

but Kenny's eq.drec_on H1 rfl worked.

[Kevin Buzzard]

simp didn't work

[Kevin Buzzard]

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

[Kevin Buzzard]

even though it was of the form X = Y

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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