Open awalterschulze opened 3 years ago
An advantage of having everything as definitions is that when we get to a formula such as
{{or p q}} {<->} or_lang {{p}} {{q}}
We can unfold or_lang
at any time.
But when we use Inductive we have to first split; intros
and then call constructor.
The same holds true for or_lang being inside another Inductive type, we first have to deconstruct the top, before we can deconstruct the operator inside.
I think this would require General Recursion as described here http://adam.chlipala.net/cpdt/html/Cpdt.GeneralRec.html
I think we will only need everything above:
Definition mergeSort : list A -> list A.
refine (Fix lengthOrder_wf (fun _ => list A)
since mergeSort also requires splitting of the list and proving that the lists are decreasing.
But then we have to see whether the proofs would be more complicated or whether we can prove some equivalance to make the proofs easier again.
Just a reference: This also relates to https://github.com/awalterschulze/regex-reexamined-coq/issues/73
Interesting.
I tried a slightly different approach, but I think it has fundamentally the same problem (maybe it even has more problems):
Fixpoint star_lang (R: lang): lang :=
fun (s: str) =>
s = [] \/
(exists s1 s2: str,
s = s1 ++ s2 /\ R s1 /\ (star_lang R s2)).
[Added later: ] It doesn't compile (gives a similar kind of error IIRC).
Did it compile?
No, it didn't...
Okay that makes sense, the s
is not structurally decreasing in a way that Coq can automatically detect.
Here was one way to get around it: https://github.com/awalterschulze/regex-reexamined-coq/blob/59bcae8115c8cb6a9d39e51f42593fec61a93c66/src/Reexamined/smart_or.v#L517 But unfolding the definition did not inspire using it for further proofs, at least way back when.
Currently we have defined our denotation of regular expression in terms of Inductive and Definition.
https://github.com/awalterschulze/regex-reexamined-coq/pull/149#discussion_r559202572
The reason so that all operators are consistently defined and we avoid the
Recursive definition is ill-formed
error when defining star_lang. Here is a recent attempt that has failed, but it does not mean that it is impossible.