# Zulip Chat Archive

## Stream: general

### Topic: congr_arg and superficially dependent functions

#### Scott Morrison (Aug 02 2018 at 14:37):

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 (Aug 02 2018 at 14:37):

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

s.

#### Scott Morrison (Aug 02 2018 at 14:37):

Here's my work so far.

#### Scott Morrison (Aug 02 2018 at 14:38):

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 (Aug 02 2018 at 14:39):

If anyone could replace the definition of `mk_congr_arg_using_dsimp`

so that `test2`

works, that would be amazing. :-)

#### Minchao Wu (Aug 03 2018 at 09:05):

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 (Aug 03 2018 at 09:23):

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 (Aug 03 2018 at 09:26):

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 (Aug 03 2018 at 09:27):

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

#### Minchao Wu (Aug 03 2018 at 09:30):

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

Last updated: May 13 2021 at 19:20 UTC