Coq - Comment appliquer une implication avec une clause de correspondance ?

Question

Je suis en train d'écrire une preuve de l'exactitude de quicksort.

Mon programme définit un type de partition, qui gère l'étape de partitionnement récursif de quicksort.

Inductive partition : Type :=
  | empty
  | join (left: partition) (pivot: nat) (right: partition).

Et une fonction qui vérifie si une partition est triée

Fixpoint p_sorted (p: partition) : bool :=
  match p with
  | empty => true
  | join l pivot r => match l, r with
    | empty, empty => true
    | join _ lp _, empty => if lp <=? pivot then p_sorted l else false
    | empty, join _ rp _ => if pivot <=? rp then p_sorted r else false
    | join _ lp _, join _ rp _ => if (lp <=? pivot) && (pivot <=? rp) then
      (p_sorted l) && (p_sorted r) else false
    end
  end.

J'ai écrit un lemme avec la structure suivante, qui stipule que les partitions gauche et droite d'une partition triée doivent également être triées. Ce lemme utilise la syntaxe "match with" pour décomposer une partition en ses sous-partitions gauche et droite :

Lemma foo : forall (p: partition), (match p with
    | empty => True
    | join left pivot right => (p_sorted p = true) -> (p_sorted left = true) /\ (p_sorted right = true)
    end).
    Proof. (* ... proof ... *) Qed.

Ce lemme est déjà prouvé.

Maintenant, je veux l'utiliser dans une nouvelle preuve, où l'hypothèse est de la forme p_sorted x = true

Comment appliquer mon précédent lemme, pour le transformer en p_sorted left = true /\ p_sorted right = true ?

apply foo ne parvient pas à s'unifier à cause de la construction de la correspondance des motifs.

Answer 1

Vous pouvez utiliser pose proof (foo x) as Hfoo . Vous devrez alors utiliser destruct x ; dans le cas où x n'est pas vide, vous aurez quelque chose à appliquer.

Cependant, une telle preuve est maladroite, aussi je recommanderais d'améliorer l'"API" de votre théorie, c'est-à-dire la façon dont foo est indiqué ; le mieux est de se spécialiser foo a la p = join ... cas.

EDIT : En fait, certaines preuves pourraient être simplifiées en révisant les définitions de p_sorted . Cette définition doit correspondre à un arbre "2-niveaux plus bas" et répéter une certaine logique, donc foo devront probablement répéter la distinction de cas à 2 niveaux. Au lieu de cela, le code pourrait être écrit de manière similaire à ce qui suit (non testé) :

Definition get_root (p : partition) : option nat :=
  match p with
  | empty => None
  | join _ pivot _ => Some pivot
  end.
Definition onat_le (p1 p2 : option nat) :=
  match p1, p2 with
  | Some n1, Some n2 => n1 <=? n2
  | _, _ => false
  end.

Fixpoint p_sorted (p: partition) : bool :=
  match p with
  | empty => true
  | join l pivot r => p_sorted l && p_sorted r && onat_le (get_root l) (Some pivot) && onat_le (Some pivot) (get_root r)
  end.

Lemma foo l pivot r:
  p_sorted (join l pivot r) = true -> p_sorted l = true /\ p_sorted r = true.
Proof.
  simpl. intros Hsort. split.
  - destruct (p_sorted l); simpl in *; easy.
  - destruct (p_sorted r); simpl in *; easy.
Qed.