countable.v: prove choose_proper

Needs the misplaced Acc_rect_max.

Add missing properness lemma for choose.

Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.

added 1 commit

• 41621c0d - Extend comment

Compare with previous version

added 1 commit

• 714d1856 - fixup! countable.v: prove choose_proper

Compare with previous version

marked this merge request as draft from Blaisorblade/stdpp@714d1856

marked this merge request as ready

Very first step towards "Pragmatic quotients" (haven't done the others yet).

That sounds interesting! I did not read that paper, so could you maybe briefly describe what you're trying to achieve in the further steps?

mentioned in issue #120

Before the full story, this is a missing lemma for the existing construction, so it should be reviewed on its own merits. I opened #120 with a sketch on the rest, but this probably belongs here on its own merits.

In fact, it's strongly inspired from eq_xchoose : extensional xchoose in https://hal.inria.fr/inria-00368403 — I should probably add an acknowledgment.

added 3 commits

• 8eb946a7 - countable.v: prove choose_proper
• 6129d673 - base.v: fix typo in comment about listset
• 2d8dd1a3 - Extend comment

Compare with previous version

added 4 commits

• ea7b2295 - countable.v: add Acc_rect_induction induction principle for Acc (MISPLACED)
• 7cea0abb - countable.v: prove choose_proper
• 2f2feee2 - base.v: fix typo in comment about listset
• 7da8577e - Extend comment

Compare with previous version

added 6 commits

• 7da8577e...15c28d70 - 4 commits from branch iris:master
• 80490f15 - countable.v: add Acc_rect_induction induction principle for Acc (MISPLACED)
• 22e73a55 - countable.v: prove choose_proper

Compare with previous version

added 1 commit

• 85322424 - countable.v: link to reference

Compare with previous version

added 2 commits

• 8d9bf669 - base.v: add Acc_rect_induction induction principle for Acc
• 077f693e - countable.v: prove choose_proper

Compare with previous version

added 2 commits

• 1858900c - Split wf_relations.v out of relations.v
• 4b7a2664 - Move Acc_dep_ind into wf_relations

Compare with previous version

added 2 commits

• 0a0c5a41 - Split wf_relations.v out of relations.v
• 702c2153 - Move Acc_dep_ind into wf_relations

Compare with previous version

added 2 commits

• 92fcbb81 - Split wf_relations.v out of relations.v
• ef75def7 - Move Acc_dep_ind into wf_relations

Compare with previous version

added 9 commits

• ef75def7...e9aae334 - 5 commits from branch iris:master
• 436ef686 - base.v: add Acc_rect_induction induction principle for Acc
• c8356804 - countable.v: prove choose_proper
• 80243e85 - Split wf_relations.v out of relations.v
• 5e1f2328 - Move Acc_dep_ind into wf_relations

Compare with previous version