well_founded_tactics

Stream: general

[Johan Commelin]

@Mario Carneiro Do you mean something like this?

meta structure well_founded_tactics :=
(rel_tac : expr → list expr → tactic unit := λ _ _, tactic.apply_instance)
(dec_tac : tactic unit := tactic.assumption)

[Johan Commelin]

For some reason that breaks gcd, so I had to add the last line to

def gcd : nat → nat → nat
| 0        y := y
| (succ x) y := have y % succ x < succ x, from mod_lt _ $ succ_pos _,
                gcd (y % succ x) (succ x)
using_well_founded { dec_tac := well_founded_tactics.default_dec_tac }

[Johan Commelin]

Which I find confusing, because the have clause is there. What more does the system want?

[Reid Barton]

I have no idea what is going on but can I just object on principle to having something called default_dec_tac which is not in fact the default value for dec_tac

[Reid Barton]

I guess you would rename default_dec_tac

[Johan Commelin]

Sure... this is WIP

[Johan Commelin]

@Mario Carneiro I think the def_replacer approach is better. But can that be done in core?

[Mario Carneiro]

The relation being used is lex well order on Sigma' (x : nat), nat

[Mario Carneiro]

default_dec_tac was simplifying it to the simple lt on nat

[Mario Carneiro]

the easy way to fix it is to take y out of the recursion, by writing

def gcd : nat → nat → nat
| 0        := \lam y, y
| (succ x) := \lam y, have y % succ x < succ x, from mod_lt _ $ succ_pos _,
                gcd (y % succ x) (succ x)

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro I think the def_replacer approach is better. But can that be done in core?

Sure, the core of def_replacer is really simple, and most of the time I talk about using def_replacer I don't actually mean using the user command but rather the idea behind it, which is to use get_attributes to get an updated list of things from the future and eval_expr to call one of them

[Johan Commelin]

Hmmm, I'm not sure if I would know how to implement this. Also, it's probably better to wait a bit till the dust has settled down of all the other changes that are going on.

[Mario Carneiro]

this can be implemented later without any mathlib breakage. I anticipate that mathlib will not change the default from assumption, and instead will explicitly call the tactic in individual definitions when needed. Changing the global default is only something that is likely to happen in third party projects

[Bryan Gin-ge Chen]

I had a go at removing default_dec_tac in a branch. Is this something we still want as a precursor to removing the order structures? The core library and leanpkg now build, but I haven't tried triaging the 20 broken tests yet.

[Johan Commelin]

Is this a dep for moving the order structures to mathlib? Whatever, I think it's good to do this anyway.

[Bryan Gin-ge Chen]

I haven't done any more work on this, but I opened a draft PR lean#288.