The Coq mailing list

[Yves Bertot <yves.bertot AT inria.fr>]

I looked at the limitations of a variety of tools.

 * Fixpoint with classical pattern-matching suffers from the explosion of cases

 * Function can't handle patterns of the form (N (_, _) _ as d1)

 * Equations can't handle patterns of the form (N (_, _) _ as d1)

So, I came up with two solutions, which are included in the attached file, that is a minimal example inspired by the discussion with Clément, but with an arbitrary minimal example that is not directly the same as Clément's code.

 

- First, the pattern (N (_, _) _ as d1) is used as an extra test before deciding if the current pattern-matching rule is to be used,  so one solution is to make this test explicit and move it out of the pattern part of the pattern-matching rule and into the computation part of the rule.

- Second, we can make explicit the fact that there are only a small number of cases by writing a specific inductive type for this purpose, write a function that maps all possible cases to these small number of cases, and use this as an auxiliary in defining the main function.  This forces us to handle termination using a well-founded relation or a measure, in the example I use a measure.  Note that we have to perform an extra proof to show termination, this proof has an explosion of cases, but they can be handled automatically (line 115 of the example).  Normally, the fact that we decompose into the relevant cases should be useful for structuring the later proofs.

Function is_valid0 is the initial one, correponding to what Clément naturally wanted to write.

Function is_valid1 is an attempt to define the same function using Function, but with a failure at the time of defining the associated lemmas.  Not good!

Function is_valid2 implements the first solution.  This seems to work.  Clément, would you like such a solution?  How does it fare for the next steps of reasoning?

Function is_valid3 implements the second solution.  Again this seems to work, but the decomposition into several sub parts makes the code less readable.  Clément: how does it fare?

It should also be interesting to explore Equations for this problem.  It also has the problem of rejecting (... as _) patterns, but the Equations package contains automatic tools for the termination proofs (automatic definition of a subterm relation, and automatic proof that it is well-founded, for instance).

I hope this helps,

Yves

---

From: "Blaudeau Clément" <clement.blaudeau AT kes.eleves.polytechnique.fr>
To: "coq-club" <coq-club AT inria.fr>
Sent: Wednesday, July 1, 2020 1:12:53 AM
Subject: Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion)

Thank you for your answer !

I’ve tried to use Function, but Coq cannot create the inductive predicate R_is_valid as soon as I add the non-trivial cases :

is_valid is defined
is_valid is recursively defined (decreasing on 1st argument)
Warning: Cannot define graph(s) for is_valid [funind-cannot-define-graph,funind]
Warning: Cannot build inversion information [funind-cannot-build-inversion,funind

However, to me, my function looks like a valid pattern matching tree without dependent type (the two issues mentioned in the documentation). The cases that are not accepted by Coq are of the following form :

| N b1 (((N b2 _ ) as d2)::((N b3 _) as d3)::nil) => (* sequence of boolean tests *) && (is_valid d2) && (is_valid d3)

Am I missing something ?

Thank you again,

Best,

Clément

Le 29/06/2020 à 20:29, Julien Forest a écrit :

On Mon, 29 Jun 2020 18:08:34 +0200
Xavier Leroy <xavier.leroy AT college-de-france.fr> wrote:

On Mon, Jun 29, 2020 at 5:39 PM Gaëtan Gilbert <
 [...]  

 [...]  

That's a very good trick, and it can be automated using Function
instead of Definition, see ttps://
coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#coq:cmd.function

Function is_valid b :=
  match b with
  | x00 | xff => true
  | _ => false (* 254 cases hidden in this _ *)
  end.

will generate the inductive predicate R_is_valid and the proofs of
equivalence with the is_valid function.

Hope this helps,

- Xavier Leroy

Just to illustrate both Gaëtan and Xavier ideas using Function.

Cheers, 

Julien Forest

 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  
 [...]  

​

a4844a0b-a89a-d714-eb77-f80fe984db4a AT kes.eleves.polytechnique.fr">

Require Import Recdef FunInd List Bool Lia.

Inductive B:=
| B0 | B1 | B2 .

Inductive A :=
| N : (B*nat) -> (list A) -> A.


Section some_context.

Variables b1 b2 b3 : A -> bool.

(* This is the function you wish to define. *)
Fixpoint is_valid0 (t : A) : bool :=
  match t with
    N((B0 | B1), _) nil => true
  | N((B0 | _), _) ((N (B2, _) _ as t1) :: (N (B2, _) _ as t2) :: nil) =>
    b1 t && is_valid0 t1 && is_valid0 t2
  | N(B2, _) ((N (B1, _) _ as t1) :: (N (B1, _) _ as t2) :: nil) =>
    b2 t && is_valid0 t1 && is_valid0 t2
  | N((B1 | B2), _) ((N(B0, _) _ as t1):: (N(B2, _) _ as t2) :: nil) =>
    b3 t && is_valid0 t1 && is_valid0 t2
  | _ => false
  end.

(* This use of Function is unsatisfactory, because none of the
  attached lemmas are generated. *)
Function is_valid1 (t : A) : bool :=
  match t with
    N((B0 | B1), _) nil => true
  | N((B0 | _), _) ((N (B2, _) _ as t1) :: (N (B2, _) _ as t2) :: nil) =>
    b1 t && is_valid1 t1 && is_valid1 t2
  | N(B2, _) ((N (B1, _) _ as t1) :: (N (B1, _) _ as t2) :: nil) =>
    b2 t && is_valid1 t1 && is_valid1 t2
  | N((B1 | B2), _) ((N(B0, _) _ as t1):: (N(B2, _) _ as t2) :: nil) =>
    b3 t && is_valid1 t1 && is_valid1 t2
  | _ => false
  end.

(* The next three test functions each correspond to one
   pattern-matching rule of is_valid0. *)
Definition rule1_test (t : A) : bool :=
  match t with
    N((B0 | _), _) ((N (B2, _) _ as t1) :: (N (B2, _) _ as t2) :: nil) => true
  | _ => false
  end.

Definition rule2_test (t : A) : bool :=
  match t with
    N(B2, _) ((N (B1, _) _ as t1) :: (N (B1, _) _ as t2) :: nil) => true
  | _ => false
  end.

Definition rule3_test (t : A) : bool :=
  match t with
    N((B1 | B2), _) ((N(B0, _) _ as t1):: (N(B2, _) _ as t2) :: nil) => true
  | _ => false
  end.

(* Now there is a single pattern-matching rule for all the cases with two
   subtrees, the body if each of the pattern-matching rule is in the
   'then' part of an if-then-else construct.  Function is happy with it
   and can detect that the function is structurally recursive. *)
Function is_valid2 (t : A) : bool :=
  match t with
    N((B0 | B1), _) nil => true
  | N((B0 | _), _) (t1 :: t2 :: nil) =>
    if rule2_test t then
      b1 t && is_valid1 t1 && is_valid1 t2
    else if rule3_test t then
      b2 t && is_valid1 t1 && is_valid1 t2
    else if rule3_test t then
           b3 t && is_valid1 t1 && is_valid1 t2
    else false
  | _ => false
  end.

(* Second solution. We devise an inductive type that captures exactly the
  cases of the intended function. *)

Inductive valid_internal_patterns : Type :=
| Case1 | Case2 (t1 t2 : A) | Case3 (t1 t2 : A) | Case4 (t1 t2 : A) | Default.

(* The function is_valid_cases computes in which case each of the tree
  will fall.  At the same time, it selects the subtrees that will be used
  in recursive calls. *)
Definition is_valid_cases (t : A) : valid_internal_patterns :=
  match t with
    N((B0 | B1), _) nil => Case1
  | N(B0, _) ((N (B2, _) _ as t1) :: (N (B2, _) _ as t2) :: nil) => Case2 t1 t2
  | N(B2, _) ((N (B1, _) _ as t1) :: (N (B1, _) _ as t2) :: nil) => Case3 t1 t2
  | N((B1 | B2), _) ((N(B0, _) _ as t1):: (N(B2, _) _ as t2) :: nil) => Case4 t1 t2
  | _ => Default
  end.

(* Now, Function will use a proof-based termination criterion instead of
  structural recursion.  Here, I choose to use size (number of N nodes) *)
Fixpoint size (t : A) :=
  match t with
    N _ l => 1 + fold_right (fun x n => Nat.add (size x) n) 0 l
  end.

Function is_valid3 (t : A) {measure size} : bool :=
  match is_valid_cases t with
    Case1 => true
  | Case2 t1 t2 => b1 t && is_valid3 t1 && is_valid3 t2
  | Case3 t1 t2 => b2 t && is_valid3 t1 && is_valid3 t2
  | Case4 t1 t2 => b3 t && is_valid3 t1 && is_valid3 t2
  | _ => false
  end.
(* Il y a 6 appels récursifs, donc 6 buts pour prouver que la mesure décroit,
  mais toutes ces preuves sont résolues automatiquement par la même tactique.
*)
all: destruct t as [[[ | | ] ?] [ | [[[ | | ] ?] ?] [ | [[[ | | ] ?] ?] [ | [[[ | | ] ?] ?]]]]]; simpl; try discriminate;
(intros t1 t2 ceq; injection ceq; intros ceq1 ceq2; rewrite <- ?ceq1, <- ?ceq2; simpl; lia).
Defined.