1
$\begingroup$

I want to define a function which decreases in one argument using < and on another structurally. What is the least painful way to do this? Among the many options (Function, Program Fixpoint, Equation) which technique should I use so that I can easily manipulate the function inside proofs?

Link for GitHub Gist with full code

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

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
.

Fixpoint parse_length (t : parse_tree) : nat :=
  match t with
  | parse_epsilon => 0
  | parse_charclass => 1
  | parse_concat t1 t2 => parse_length t1 + parse_length t2
  | parse_union_l t => parse_length t
  | parse_union_r t => parse_length t
  | parse_star_nil => 0
  | parse_star_cons t1 t2 => parse_length t1 + parse_length t2
end.

Fail Fixpoint all_parse_trees (w : list A) (start len : nat) (r : Regex) : list parse_tree :=
  match r with
  | Epsilon => [parse_epsilon]
  | CharClass p => match nth_error w start with
                    | Some a => if p a then [parse_charclass] else []
                    | None => []
                    end
  | Concat r1 r2 => flat_map (fun t1 => map (fun t2 => parse_concat t1 t2) (all_parse_trees w (start + parse_length t1) (len - parse_length t1) r2)) (all_parse_trees w start len r1)
  | Union r1 r2 => map (fun t => parse_union_l t) (all_parse_trees w start len r1) ++ map (fun t => parse_union_r t) (all_parse_trees w start len r2)
  | Star r => 
    parse_epsilon :: 
      (flat_map 
      (fun t1 => map (fun t2 => parse_star_cons t1 t2) (all_parse_trees w (start + parse_length t1) (len - parse_length t1) (Star r) ))
      (filter (fun t => ltb 0 (parse_length t)) (all_parse_trees w start len r)))
      end.

My attempt: I tried to define the order used by this recursion explicitly.

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

Definition regex_nat_lex (rn : Regex * nat) (rm : Regex * nat) : Prop :=
  match rn, rm with
  | (r1, n1), (r2, n2) => 
    regex_struct r1 r2 \/ (r1 = r2 /\ n1 < n2)
  end.

However, Coq does not seem to give me enough context so that I can prove the obligations:

Program Fixpoint all_parse_trees (w : list A) (start : nat) (rn : Regex * nat) {wf regex_nat_lex rn} : list parse_tree :=
  match rn with
  | (Epsilon, _) => [parse_epsilon]
  | (CharClass p, _) => match nth_error w start with
                      | Some a => if p a then [parse_charclass] else []
                      | None => []
                      end
  | (r1 · r2, len) => flat_map (fun t1 => map (fun t2 => parse_concat t1 t2) (all_parse_trees w (start + parse_length t1) (r2, (len - parse_length t1)))) (all_parse_trees w start (r1, len))
  | (r1 ∪ r2, len) => map (fun t => parse_union_l t) (all_parse_trees w start (r1, len)) ++ map (fun t => parse_union_r t) (all_parse_trees w start (r2, len))
  | ((r *), len) => 
    parse_epsilon :: 
      (flat_map 
      (fun t1 => map (fun t2 => parse_star_cons t1 t2) (all_parse_trees w (start + parse_length t1) ((r *), (len - parse_length t1))))
      (filter (fun t => ltb 0 (parse_length t)) (all_parse_trees w start (r, len))))
      end.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
Admitted.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
Admitted.

For the first admitted goal, Coq does not seem to be able to notice that the function is being applied to arguments which satisfy a certain filter.

$\endgroup$
0

2 Answers 2

2
$\begingroup$

I rephrased the * case into :

 | ((r *), len) => 
       parse_epsilon :: 
         (flat_map 
            (fun t1 => 
               match parse_length t1, len  
               with 0, _ | _, 0  => [] |
                 l , len => 
                   map 
                     (fun t2 => parse_star_cons t1 t2)
                     (all_parse_trees w (start + l) ((r *), (len - l)))
                      end )) 
            (all_parse_trees w start (r, len))

The main change is to check whether parse_length t1 > 0 before the recursive call on r *.
It fixes also the fact that n - S p < n may be false (take for instance n = 0).

I didn't verify whether this new version is exactly what you wanted. Could you check it? All the proof obligations but the last one are easily proved. For this last obligation, I suggest replacing the ad-hoc definition of the lexicographic product with one of Coq's library and benefit from the theorem "the lexicographic product of two well-founded relations is well-founded too".

https://coq.inria.fr/distrib/current/stdlib/Coq.Wellfounded.Lexicographic_Product.html

$\endgroup$
3
0
$\begingroup$

If you do not want to alter the structure of your program, but merely want to propagate some information inside a list iterator, there is a common pattern, I'll illustrate with map here:

Section MapInP.
  Context {A B : Type}.
  Context {P : A -> Type}.
  Context (f : forall (x : A), P x -> B).

  Program Fixpoint map_InP (l : list A) (H : forall x, In x l -> P x) : list B :=
    match l with
    | nil => nil
    | cons x xs => cons (f x (H x _)) (map_InP xs (fun x inx => H x _))
    end.
  Next Obligation.
    now left.
  Qed.
  Next Obligation.
    now right.
  Qed.
    
End MapInP.

Lemma map_InP_spec {A B : Type} {P : A -> Type} (f : A -> B) (l : list A) (H : forall x, In x l -> P x) :
  map_InP (fun (x : A) (_ : P x) => f x) l H = List.map f l.
  Proof.
    remember (fun (x : A) (_ : P x) => f x) as g.
    induction l ; cbn ; try easy.
    f_equal.
    - now rewrite Heqg.
    - now rewrite IHl.
  Qed.

The idea is that you can now replace uses of map f l with map_InP (fun x p => f x) l _, which will give you an extra hypothesis P inside of the map, that you can typically use for termination purposes, at the cost of showing when you call map_InP that all elements of your list satisfy the predicate. The lemma map_InP_spec can be used to replace usage of map_InP by map when you want to reason about your function.

In your particular case, you'll probably need to have a variant of flatmap of the same flavour, and use that.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.