Timeline for Eliminating dependent destruction in Coq
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 6, 2023 at 20:10 | answer | added | Circuit Craft | timeline score: 2 | |
| Sep 6, 2023 at 8:55 | comment | added | Meven Lennon-Bertrand♦ |
I figured it would be something like this, and I think that, just like arith_formula, having it around as a black-box constant would make the inductive look more like what you are interested in. But anyway, since you've solved your problem that's irrelevant. Maybe you could self-answer your question though, outlining the main steps that unlocked you? That's good SE practice, so that others finding your question when faced with similar issues can solve theirs too.
|
|
| Sep 5, 2023 at 21:22 | comment | added | Circuit Craft |
@MevenLennon-Bertrand Thank you! I'd already tried Scheme, which didn't work, but combining remember and using P : arith_formula -> Prop worked perfectly! The base case, by the way, is quantifier_free f -> Sigma 0 f and likewise for Pi 0 f, but that is its own inductive definition, which I felt would overcomplicate the problem.
|
|
| Sep 5, 2023 at 17:41 | comment | added | Meven Lennon-Bertrand♦ |
Another remark: dependently-typed induction principles on propositions (like the one you are trying to prove) are in general useless. This is because of proof irrelevance, which implies that it is impossible to define a function P : forall f, (H : Sigma f (S n)) -> Prop which is not constant in its second argument. Thus, it is probably enough to prove a non-dependent induction principle, ie one with P : arith_formula -> Type. Note that this is why by default Coq does not generate a dependent induction principle for propositions.
|
|
| Sep 5, 2023 at 17:38 | comment | added | Meven Lennon-Bertrand♦ |
Are you aware of Scheme and Combined Scheme to generate mutual induction principles? In your case, I'm not sure what the exact solution should be, because as it is both your inductive predicates are empty (since you are missing a base case). But I would advise you to use Combined Scheme to generate a mutual induction principle, together with a possible fiddling with remember to turn the S n index into a generic variable + an equality proof.
|
|
| Sep 5, 2023 at 16:37 | comment | added | Trebor♦ |
I don't have enough brainpower to flesh this out but IIUC yes you can prove this in theory without the axiom, because no variable in the index appears twice, and assuming arith_formula is an inductive type and fexis etc are constructors, everything is in order for pattern matching without K. How to efficiently do that in practice though I do not have enough expertise to say.
|
|
| Sep 5, 2023 at 16:21 | history | asked | Circuit Craft | CC BY-SA 4.0 |