Convoy Pattern + Sigma Types + Equations

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

(**

Jason's Solution: Use with pattern in Equations instead of Convoy pattern.

**)

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

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) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t, btc')) _ := exist _ (Some (parse_union_l t, btc')) _
};
decode_aux (Union _ e, true :: btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t, btc')) _ := exist _ (Some (parse_union_r t, btc')) _
};
decode_aux (Concat e f, btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t1, btc')) _ with decode_aux (f, btc') := {
        | exist _ None _ := exist _ None _;
        | exist _ (Some (t2, btc'')) _ := exist _ (Some (parse_concat t1 t2, btc'')) _
    }
};
decode_aux (Star _, []) := exist _ None _;
decode_aux (Star _, true :: btc) := exist _ None _;
decode_aux (Star e, false :: btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t1, btc')) _ with decode_aux (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.
lia.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
left. constructor.
Defined.
Next Obligation.
right. simpl.
lia.
Defined.
Next Obligation.
lia.
Defined. (* What is happening when invoking this Defined?! *)

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

Fail 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) as ebtc1 return decode_aux (e, btc) = ebtc1 -> decode_aux_type _ with
    | exist _ (Some (t, btc')) _ => fun Heq => exist _ (Some (parse_union_l t, btc')) _
    | exist _ None _ => fun Heq => exist _ None _
    end) eq_refl;
decode_aux (Union _ e, true :: btc) :=
    (match decode_aux (e, btc) as ebtc1 return decode_aux (e, btc) = ebtc1 -> decode_aux_type _ with
    | exist _ None _ => fun Heq => exist _ None _
    | exist _ (Some (t, btc')) _ => fun Heq => exist _ (Some (parse_union_r t, btc')) _
    end) eq_refl;
decode_aux (Concat e f, btc) :=
    (match decode_aux (e, btc) as ebtc1 return decode_aux (e, btc) = ebtc1 -> decode_aux_type _ with
    | exist _ None _ => fun Heq => exist _ None _
    | exist _ (Some (t1, btc')) _ =>
        (match decode_aux (f, btc') as ebtc2 return decode_aux (f, btc') = ebtc2 -> decode_aux_type _ with
        | exist _ None _ => fun Heq => exist _ None _
        | exist _ (Some (t2, btc'')) _ => fun Heq => exist _ (Some (parse_concat t1 t2, btc'')) _
        end) eq_refl
    end) eq_refl;
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) as ebtc1 return decode_aux (e, btc) = ebtc1 -> decode_aux_type _ with
    | exist _ None _ => fun Heq => exist _ None _
    | exist _ (Some (t1, btc')) _ =>
        (match decode_aux (Star e, btc') as ebtc2 return decode_aux (Star e, btc') = ebtc2 -> decode_aux_type _ with
        | exist _ None _ => fun Heq => exist _ None _
        | exist _ (Some (t2, btc'')) _ => fun Heq => exist _ (Some (parse_star_cons t1 t2, btc'')) _
        end) eq_refl
    end) eq_refl.

(**

The above fails with the following error message:

(unable to find a well-typed instantiation for "?P": cannot ensure that
"match o0 with
 | Some p => let (_, btc) := p in length btc <= length (snd (f, btc'))
 | None => True
 end" is a subtype of
"(fun o : option (parse_tree * list bool) =>
  match o with
  | Some p => let (_, btc) := p in length btc <= length (snd (f, btc'))
  | None => True
  end) (Some (t2, btc''))").

*)