congr_arg and superficially dependent functions

Stream: general

[Scott Morrison]

I'm having trouble constructing congr_arg expressions, where the function superficially looks like a dependent function, but after some definitionally unfolding you can see that it isn't really.

[Scott Morrison]

I've worked out how to get around this in interactive mode, but I can't do it with exprs.

[Scott Morrison]

Here's my work so far.

[Scott Morrison]

def F : Π n : ℕ, Type := λ n, ℕ
def G : Π n : ℕ, F n := λ n, begin dunfold F, exact 0 end

lemma test (m n : ℕ) (w : m = n) : G n == G m :=
begin
  -- This doesn't work, because `G` looks like a dependent function
  success_if_fail {
    have h := congr_arg G w
  },
  -- In fact it isn't really, and we can discover this with `dsimp`.
  let g := G,
  dsimp [F] at g,
  -- Now we can use congr_arg.
  let h := congr_arg g w,
  dsimp [g] at h,
  rw h,
end

-- Now I want to do this via `expr` munging:

open tactic

meta def mk_congr_arg_using_dsimp (G W : expr) (F : name) : tactic expr :=
-- I have no idea how to achieve this: this doesn't work, but is my best guess.
do
  s ← simp_lemmas.mk_default,
  t ← infer_type G,
  t' ← s.dsimplify [F] t {fail_if_unchanged := ff},
  trace t',
  to_expr ```(congr_arg (%%G : %%t') %%W)

lemma test2 (m n : ℕ) (w : m = n) : G n == G m :=
begin
  let h := by tactic.get_local `w >>= λ W, mk_congr_arg_using_dsimp `(G) W `F,
  rw h,
end

[Scott Morrison]

If anyone could replace the definition of mk_congr_arg_using_dsimp so that test2 works, that would be amazing. :-)

[Minchao Wu]

A quick solution:

meta def mk_congr_arg_using_dsimp (G W : expr) (F : name) : tactic unit :=
do
  eg ← to_expr ```(λ n:nat, id 0),
  t ← infer_type G,
  s ← simp_lemmas.mk_default,
  t' ← s.dsimplify [F] t {fail_if_unchanged := ff},
  definev `g t' eg,
  eg ← get_local `g,
  eeq ← to_expr ```(%%G = %%eg),
  assert `h eeq,
  try reflexivity

lemma test2 (m n : ℕ) (w : m = n) : G n == G m :=
begin
  tactic.get_local `w >>= λ W, mk_congr_arg_using_dsimp `(G) W `F,
  rw h
end

[Minchao Wu]

The attempt is to force lean to be aware that the two types of G collapse, however (%%G : %%t') doesn't do the trick. This introduces an additional local hypothesis which has the non-dependent type and proves that it is just G.

[Scott Morrison]

Thanks @Minchao Wu. In the meantime I'd come up with my own solution:

-- Sometimes `mk_congr_arg` fails, when the function is 'superficially dependent'.
-- This hack first dsimplifies the function before building the `congr_arg` expression.
-- Unfortunately it creates a dummy hypothesis that I can't work out how to avoid or dispose of cleanly.
meta def mk_congr_arg_using_dsimp (G W : expr) (u : list name) : tactic expr :=
do
  s ← simp_lemmas.mk_default,
  t ← infer_type G,
  t' ← s.dsimplify u t {fail_if_unchanged := ff},
  tactic.definev `_mk_congr_arg_aux t' G,
  to_expr ```(congr_arg _mk_congr_arg_aux %%W)

which is fairly similar!

[Scott Morrison]

The next question is how to achieve this without making the local hypothesis, so this tactic doesn't pollute the current goal.

[Minchao Wu]

Yeah I'm also wondering if there is a neater solution :)