Definition vs Inductive

[awalterschulze]

Currently we have defined our denotation of regular expression in terms of Inductive and Definition.

#149 (comment)

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.

Fixpoint star_lang (R: lang) (s: str) {struct s}: Prop :=
  match s with
  | [] => True
  | (a::s') =>
    forall (p q: str),
    (a::p) ++ q = s' /\
    (a::p) \in R /\
    q \in star_lang R
  end.

Recursive definition of star_lang is ill-formed.
In environment
star_lang : lang -> str -> Prop
R : lang
s : str
a : alphabet
s' : list alphabet
p : str
q : str
Recursive call to star_lang has principal argument equal to 
"q" instead of "s'".
Recursive definition is:
"fun (R : lang) (s : str) =>
 match s with
 | [] => True
 | a :: s' =>
     forall p q : str,
     (a :: p) ++ q = s' /\ (a :: p) \in R /\ q \in star_lang R
 end".

Note: this definition has an error at (a::p) ++ q = s', which should be p ++ q = s' , but even with this fix the error still happens.

[awalterschulze]

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.

[awalterschulze]

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.

[awalterschulze]

Just a reference: This also relates to #73

[Nielius]

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).

[awalterschulze]

Did it compile?

[Nielius]

No, it didn't...

[awalterschulze]

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.