Convoy Pattern + Sigma Types + Equations

Recursion.v

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Require Import Arith.

Import ListNotations.

Require Import Coq.Init.Nat.
Require Import Lia.

From Equations Require Import Equations.
Require Import Coq.Program.Wf.

Declare Scope regex_scope.
Open Scope regex_scope.

Section Regex.

Variable (A : Type).

Inductive Regex : Type :=
| Epsilon : Regex
| CharClass : (A -> bool) -> Regex
| Concat : Regex -> Regex -> Regex
| Union : Regex -> Regex -> Regex
| Star : Regex -> Regex
.

Definition ε := Epsilon.
Infix "·" := Concat (at level 60, right associativity) : regex_scope.
Infix "∪" := Union (at level 50, left associativity) : regex_scope.
Notation "r *" := (Star r) (at level 40, no associativity) : regex_scope.

Inductive parse_tree : Type :=
| parse_epsilon : parse_tree
| parse_charclass : parse_tree
| parse_concat : parse_tree -> parse_tree -> parse_tree
| parse_union_l : parse_tree -> parse_tree
| parse_union_r : parse_tree -> parse_tree
| parse_star_nil : parse_tree
| parse_star_cons : parse_tree -> parse_tree -> parse_tree
.

Inductive regex_struct : Regex -> Regex -> Prop :=
| regex_struct_concat_l : forall (r1 r2 : Regex),
    regex_struct r1 (r1 · r2)
| regex_struct_concat_r : forall (r1 r2 : Regex),
    regex_struct r2 (r1 · r2)
| regex_struct_union_l : forall (r1 r2 : Regex),
    regex_struct r1 (r1 ∪ r2)
| regex_struct_union_r : forall (r1 r2 : Regex),
    regex_struct r2 (r1 ∪ r2)
| regex_struct_star : forall (r : Regex),
    regex_struct r (r *)
.

#[ global ] Instance WF_lt_regex : WellFounded regex_struct.
intros r. induction r; constructor; intros.
  1, 2 : inversion H.
  + inversion H; subst; auto.
  + inversion H; subst; auto.
  + inversion H; subst; auto.
Defined.

#[ global ]  Instance length_lt_wf {X} : WellFounded (fun l1 l2 => @length X l1 < length l2).
Proof.
  intro l.
  remember (length l) as n.
  revert l Heqn.
  induction n using lt_wf_ind; intros.
  constructor. intros l' Hlen.
  apply H with (m := length l').
  - lia.
  - reflexivity. 
Defined.

#[ global ]  Instance decode_order_wf : 
  @WellFounded (Regex * list bool) 
  (slexprod _ _ regex_struct (fun l m => length l < length m)).
Proof.
  apply wf_slexprod.
  - apply WF_lt_regex.
  - apply length_lt_wf.
Defined. 

Fixpoint bitcode (t : parse_tree) : list bool :=
  match t with
  | parse_epsilon => []
  | parse_charclass => []
  | parse_concat t1 t2 => bitcode t1 ++ bitcode t2
  | parse_union_l t => false :: bitcode t
  | parse_union_r t => true :: bitcode t
  | parse_star_nil => [true]
  | parse_star_cons t1 t2 => false :: bitcode t1 ++ bitcode t2
  end.

(* decode_aux_1 is intended to be an inverse of bitcode *)

Equations decode_aux_1 (ebtc : Regex * list bool) : option (parse_tree * list bool)
  by wf ebtc (slexprod _ _ regex_struct (fun l m => length l < length m)) :=
decode_aux_1 (Epsilon, btc) := Some (parse_epsilon, btc);
decode_aux_1 (CharClass p, btc) := Some (parse_charclass, btc);
decode_aux_1 (Union _ _, []) := None;
decode_aux_1 (Union e _, false :: btc) := 
    match decode_aux_1 (e, btc) with
    | Some (t, btc') => Some (parse_union_l t, btc')
    | None => None
    end;
decode_aux_1 (Union _ e, true :: btc) :=
    match decode_aux_1 (e, btc) with
    | Some (t, btc') => Some (parse_union_r t, btc')
    | None => None
    end;
decode_aux_1 (Concat e f, btc) :=
    match decode_aux_1 (e, btc) with
    | Some (t1, btc') =>
        match decode_aux_1 (f, btc') with
        | Some (t2, btc'') => Some (parse_concat t1 t2, btc'')
        | None => None
        end
    | None => None
    end;
decode_aux_1 (Star e, []) := None;
decode_aux_1 (Star e, true :: btc) := None;
decode_aux_1 (Star e, false :: btc) :=
    match decode_aux_1 (e, btc) with
    | Some (t1, btc') =>
        match decode_aux_1 (Star e, btc') with
        | Some (t2, btc'') => Some (parse_star_cons t1 t2, btc'')
        | None => None
        end
    | None => Some (parse_star_nil, btc)
    end.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
right. 
(* we have lost the connection between btc' and btc *)
Admitted.

(**

We need to make sure that two pieces of information are propagated, so that we can complete the proof:
(1) When using the match statement, [match decode_aux_1 (e, btc) with | Some (t, btc') => ... end], we need the equation saying [match decode_aux_1 (e, btc) = Some (t, btc')]
(2) We need to be able to propagate the information that if [decode_aux_1 (e, btc) = Some (t, btc')] then [length btc' < length btc]

For the first one, we will use the "convoy pattern", i.e, we will write something like this:

(match decode_aux (e, btc) as res return decode_aux (e, btc) = res -> ... with
| Some (t, btc') => fun Heq => ...
| None => fun Heq => ...
end) eq_refl.

For the second one, we will use Sigma types so that the information is carried around. So, instead of having 

decode_aux_1 (ebtc : Regex * list bool) : option (parse_tree * list bool)

we will have

decode_aux (ebtc : Regex * list bool) : 
    {o : option (parse_tree * list bool)  | match o with | Some (t, btc') => length btc' < length (snd ebtc) | None => True end }

**)

Definition decode_aux_type (orb : Regex * list bool) :=
  { o : option (parse_tree * list bool) | (match o with | Some (t, btc) => length btc <= length (snd orb) | None => True end) }.

(* The trick is to pull the matches apart. We do not actually need dependent pair equality,
   it is sufficient to know that the arguments are equal.
   It seems like Equations tries (and fails to) properly handle equality of dependent pairs.
   Unfortunately, dependent pair equality is tricky (such pairs are not in general injective in
   their second argument, this is equivalent to UIP), so likely Equations fails to do things properly somewhere. *)


Equations decode_aux (ebtc : Regex * list bool) : 
  decode_aux_type ebtc
  by wf ebtc (slexprod _ _ regex_struct (fun l m => length l < length m)) :=
decode_aux (Epsilon, btc) := exist _ (Some (parse_epsilon, btc)) _;
decode_aux (CharClass p, btc) := exist _ (Some (parse_charclass, btc)) _;
decode_aux (Union _ _, []) := exist _ None _;
decode_aux (Union e _, false :: btc) := 
    match decode_aux (e, btc) with
    | exist _ mo _ => match mo as mo' return mo = mo' -> _ with
        | Some (t, btc') => fun Heq => exist _ (Some (parse_union_l t, btc')) _
        | None  => fun Heq => exist _ None _
      end eq_refl
    end;
decode_aux (Union _ e, true :: btc) :=
    match decode_aux (e, btc) with
    | exist _ mo _ => match mo as mo' return mo = mo' -> _ with
        | None  => fun Heq => exist _ None _
        | Some (t, btc') => fun Heq => exist _ (Some (parse_union_r t, btc')) _
      end eq_refl
    end;
decode_aux (Concat e f, btc) :=
    match decode_aux (e, btc) with
    | exist _ mo1 _ => match mo1 as mo1' return mo1 = mo1' -> _ with
        | None => (fun Heq1 => exist _ None _ )
        | Some (t1, btc') => fun Heq1 =>
          (match decode_aux (f, btc') with
            | exist _ mo2 _ => match mo2 as mo2' return mo2 = mo2' -> _ with
              | None => fun Heq2 => exist _ None _
              | Some (t2, btc'') => fun Heq2 => exist _ (Some (parse_concat t1 t2, btc'')) _
            end eq_refl end)
    end eq_refl end;
decode_aux (Star e, []) := exist _ None _;
decode_aux (Star e, true :: btc) := exist _ None _;
decode_aux (Star e, false :: btc) :=
    (match decode_aux (e, btc) with
    | exist _ mo1 _ => match mo1 as mo1' return mo1 = mo1' -> _ with
      | None => fun Heq1 => exist _ None _
      | Some (t1, btc') => fun Heq1 => 
        (match decode_aux (Star e, btc') with
        | exist _ mo2 _ => match mo2 as mo2' return mo2 = mo2' -> _ with
          | None => fun Heq => exist _ None _
          | Some (t2, btc'') => fun Heq => exist _ (Some (parse_star_cons t1 t2, btc'')) _
        end eq_refl end)
    end eq_refl end). 
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
eapply Nat.le_trans; eassumption.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
right. simpl. eapply le_n_S. assumption.
Defined.
Next Obligation.
eapply Nat.le_le_succ_r, Nat.le_trans; eassumption.
Defined.

(* This is the proper way of defining this with Equations,
   which has all the magic for "advanced" pattern-matching built-in.
   Specifically, it does "remember" the connection between the fact that the result is 
   `Some (t, btc')` and that we have a further predicate on that match.
   Sadly, this does not work -- Equations timeouts after solving the last definition. *)

Equations decode_aux2 (ebtc : Regex * list bool) : 
  decode_aux_type ebtc
  by wf ebtc (slexprod _ _ regex_struct (fun l m => length l < length m)) :=
decode_aux2 (Epsilon, btc) := exist _ (Some (parse_epsilon, btc)) _;
decode_aux2 (CharClass p, btc) := exist _ (Some (parse_charclass, btc)) _;
decode_aux2 (Union _ _, []) := exist _ None _;
decode_aux2 (Union e _, false :: btc) with decode_aux2 (e, btc) := {
  | exist _ (Some (t, btc')) _ := exist _ (Some (parse_union_l t, btc')) _
  | exist _ None _ := exist _ None _
};
decode_aux2 (Union _ e, true :: btc) with decode_aux2 (e, btc) := {
  | exist _ None _ := exist _ None _
  | exist _ (Some (t, btc')) _ := exist _ (Some (parse_union_r t, btc')) _
};
decode_aux2 (Concat e f, btc) with decode_aux2 (e, btc) := {
  | exist _ None _ := exist _ None _
  | exist _ (Some (t1, btc')) _ with decode_aux2 (f, btc') := {
    | exist _ None _ := exist _ None _
    | exist _ (Some (t2, btc'')) _ := exist _ (Some (parse_concat t1 t2, btc'')) _
  }
};
decode_aux2 (Star e, []) := exist _ None _;
decode_aux2 (Star e, true :: btc) := exist _ None _;
decode_aux2 (Star e, false :: btc) with decode_aux2 (e, btc) := {
  | exist _ None _ := exist _ None _
  | exist _ (Some (t1, btc')) _ with decode_aux2 (Star e, btc') := {
    | exist _ None _ := exist _ None _
    | exist _ (Some (t2, btc'')) _ := exist _ (Some (parse_star_cons t1 t2, btc'')) _
  }
}.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
eapply Nat.le_trans; eassumption.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
right. simpl. eapply le_n_S. assumption.
Defined.
Next Obligation.
eapply Nat.le_le_succ_r, Nat.le_trans; eassumption.
Timeout 60 Defined.