The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

You may convert is_valid to an inductive type, that way it only has 
constructors for the cases you want and you can destruct it directly.
see attached file for an example

Gaëtan Gilbert

On 29/06/2020 16:46, Blaudeau Clément wrote:
> Hi Everyone,
> I'm currently working to prove results on a fonction that uses several levels 
> of nested pattern matching and it generates *a lot* of trivial subgoals, to 
> the point that every proof takes several minutes to go through.
>
> ##### High level view of the problem
>
> I have an inductive type with ~ 50 constructors, and nested pattern matching 
> on lists of that type. The nested pattern matching is translated into several 
> levels of normal pattern matching with one case that is interesting and 49 
> useless cases. To build proofs on my function, I would like to be able to 
> extract easily the interesting cases, and quickly drop all useless cases. Is 
> there automated ways of doing that ? Just destruct the match expressions and 
> using `congruence` is too slow.
>
> ##### More details
>
> I have a function  `is_valid : A -> bool`, and I want to prove results of the 
> form `is_valid a = true -> P`, where `A` is an inductive type of the form
> ```Coq
> Inductive A := | N : B -> (list A) -> A . % N is the only constructor
> ```
> And `B` is also an inductive type **with around 50 constructors**.
> The problem is that, in the `is_valid` function, I have nested pattern 
> matching (on the list) like
> ```Coq
> | N b1 (N b2 [])::(N b3 [])::_ => (f b1 b2 b3) % some property computed using 
> b1 b2 b3
> ```
> generates huge patterns, because the internal translation of nested patterns 
> is to create several levels of patterns. As my type `B` has 50 constructors, 
> each level of pattern matching generates **a lot** of subgoals and slows down 
> the proofs.
>
> Is there a simple way to say that if `is_valid a = true` then all the possible 
> cases are only the ones of the main pattern matching, without having to break all 
> sub-levels of matching using `congruence` everywhere ? Just doing an `unfold` of 
> the `is_valid` function takes ~2 min on my computer. The dream would be that 
> `is_valid a = true -> P` could be split into the few subgoals of the form `.. /\ 
> (f b1 b2 b3) -> P /\ ...`
>
> Thank you for your help !
> Clément
>
> PS: I could write a big theorem saying that for any property P, but I'm 
> looking for an automated way of doing it
Require Import Init.Byte.

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

Lemma some_lemma : forall b, is_valid b = true -> b = x00 \/ b = xff.
Proof.
  intros b v;destruct b;try discriminate v. (* 254 cases discriminated away *)
  - left;reflexivity.
  - right;reflexivity.
Qed.

Inductive is_valid' : byte -> Prop :=
| valid00 : is_valid' x00
| validff : is_valid' xff
.

Lemma some_lemma' : forall b, is_valid' b -> b = x00 \/ b = xff.
Proof.
  intros b v;destruct v.
  - left;reflexivity.
  - right;reflexivity.
Qed.

(* If you want to recover decidability of validity you still can
   (here by hand, or you can use some ssr stuff for decidable properties) *)
Definition valid'_checker (b:byte) : { v:bool | v=true <-> is_valid' b}.
Proof.
  destruct b;try (exists true; split; intros _;constructor).
  (* 254 remaining cases *)
  all: exists false;split;[discriminate|intros v;inversion v].
 (* note that each inversion builds a 2-cases match *)
Defined.