4
votes
Accepted
How to use Modus Ponens in L axiomatic system
I would suggest two improvements to your code:
Use implicit arguments, so that you can tell Coq which rule, axiom or lemma to apply without having to specify how to apply it.
Do not use ...
- 10.1k
3
votes
How does Coq guess `i` is decreasing?
The mechanism in charge of detecting whether a recursive call is "decreasing" is called the guard condition. Unfortunately, in order to allow for subtle examples like yours, it is quite a ...
- 5,645
2
votes
Accepted
Is it possible to simplify/normalize nat arithmetic expressions in Coq?
The ring_simplify tactic handles normalisation of ring expression just fine (the ring tactic basically simplifies expressions ...
- 5,645
2
votes
Extensional sets in Coq and induction
Indeed, what you want to do is not directly possible: defining an inductive type mutually with a function out of it (here, the order-deciding function), is a complex type-theoretic feature known as ...
- 5,645
Only top scored, non community-wiki answers of a minimum length are eligible