nat: least common multiple

[Alizter]

No description provided.

[jdchristensen]

It would be good to figure out why typeclass search spins if you use rapply here. We must have some bad choices of instances.

[Alizter]

FTR:

Calling typeclass resolution with flags: depth = 5,unique = false,fail = false
1: looking for (0 < ?k) with backtracking
1.1: simple apply @lt_succ_r on (0 < ?k), 1 subgoal(s)
1.1-1 : (0 < ?m0)
1.1-1: looking for (0 < ?m0) with backtracking
1.1-1.1: simple apply @lt_succ_r on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1 : (0 < ?m0)
1.1-1.1-1: looking for (0 < ?m0) with backtracking
1.1-1.1-1.1: simple apply @lt_succ_r on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1 : (0 < ?m0)
1.1-1.1-1.1-1: looking for (0 < ?m0) with backtracking
1.1-1.1-1.1-1.1: simple apply @lt_succ_r on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.1-1 : (0 < ?m0)
1.1-1.1-1.1-1.1-1: looking for (0 < ?m0) with backtracking
1.1-1.1-1.1-1.1-1.1: simple apply @lt_succ_r on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.1-1 : (0 < ?m0)
1.1-1.1-1.1-1.1-1.2: unfold lt on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.2-1 : (1 <= ?m0)
1.1-1.1-1.1-1.1-1.3: simple apply lt_is_leq on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.3-1 : (1 <= ?m0)
1.1-1.1-1.1-1.2: unfold lt on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.2-1 : (1 <= ?m0)

lt_succ_r is used in a few places. I'll see about pruning it so it doesn't get used too often.

[Alizter]

Fixed by making lt_succ_r lower priority. It was being used somewhere for FinNat and caused an error, but this was fixed by explicitly giving the expected instance.

[jdchristensen]

But won't it still potentially loop if other instances don't solve the goal? Would it be better to constrain it with Hint Mode so that it only applies when the goal is of the form ?n < constructor?

BTW, this part

1.1-1.1-1.1-1.1-1.2: unfold lt on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.2-1 : (1 <= ?m0)
1.1-1.1-1.1-1.1-1.3: simple apply lt_is_leq on (0 < ?m0), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.3-1 : (1 <= ?m0)

is because of

#[export] Hint Unfold lt : typeclass_instances.
Global Instance lt_is_leq n m : leq n.+1 m -> lt n m | 100 := idmap.

Isn't the Hint Unfold line redundant given the second line? Or vice versa? (And same for the other two inequalities.)

[Alizter]

I'll remove the instances, the unfold hint is more general. For example, IsHProp (a < b) can be solved.

[Alizter]

I wasn't able to get Hint Mode to work here.

[jdchristensen]

I see you are using divides_l and divides_r for the next few results, but maybe it's better to put the thing before or after the word "divides"? OTOH, if this is how it was done systematically in the rest of the file, I guess it's ok.

[Alizter]

I always put it after given that's how we do it elsewhere. Naming things is hard, but I guess its better to be consistent. Iff doesn't follow this convention, but maybe it should for consistency.

[jdchristensen]

Here I guess that last _l indicates that the first argument of lcm is "special" in that it is the n that appears on the left of the divides relation? Not obvious, but reasonable.

[Alizter]

Yes that's the correct interpretation.