Library coq5_eqnatb

Énoncé complet : voir TD.

Preuve d'équivalence entre égalité des entiers et eqnatb valant true

eqnatb renvoie true ssi ses arguments représentent le même entier naturel

Égalité booléenne entre deux entiers

Observation clé : dans l'appel récursif, le second paramètre ne reste pas fixé à n2

Fixpoint eqnatb n1 n2 :=
   match n1,n2 with
  | O,O ⇒ true
  | S n1', S n2' ⇒ eqnatb n1' n2'
  | _,_ ⇒ false
  end.

Le sens le plus facile (récurrence triviale)

Lemma eqnatb_eq1 : ∀ n, eqnatb n n = true.
Proof.
  intro n; induction n as [ | n' Hn'].
  - reflexivity.
  - apply Hn'.
Qed.

Démo surprise (1) : preuve fournie par un programme récursif

Fixpoint eqnatb_eq1_fct n : eqnatb n n = true :=
  match n with
  | 0 ⇒ eq_refl
  | S n' ⇒ eqnatb_eq1_fct n'

Observer la décroissance structurelle

end.

Lemma eqnatb_eq2 : ∀ n1 n2, n1 = n2 → eqnatb n1 n2 = true.
Proof.
Admitted.

Le sens le plus difficile (récurrence quantifiée + preuve par cas)

Lemma true_false_eg : true = false → ∀ n1 n2 : nat, n1 = n2.
Admitted.

C'est l'autre direction qui nous intéresse, on peut la démontrer à partir du lemme précédent

Lemma false_true_eg : false = true → ∀ n1 n2 : nat, n1 = n2.
Proof.
intro eft. intros n1 n2.
apply true_false_eg.

Bien comprendre ce apply et terminer la preuve

Admitted.

Dans la suite, plutôt que rewrite il est intéressant d'employer un apply de S_equal. Voir exemple d'utilisation plus bas.

Lemma S_equal : ∀ x y : nat, x = y → S x = S y.
Proof.

À démontrer (facile)

Admitted.

Remarque : f_equal est une version générale de ce lemme

Check (f_equal S).

Lemma eq_eqnatb : ∀ n1 n2, eqnatb n1 n2 = true → n1 = n2.
Proof.
intros n1.
Admitted.

Démo surprise (2)

Reset eq_eqnatb.

Échauffement : neutralité de 0 à droite de +

Mise au point avec refine

Fixpoint plus_0_r n : n + 0 = n.
Proof.
  refine (
      match n with
      | 0 ⇒ eq_refl
      | S n' ⇒ _
      end).
  - cbn [plus]. apply S_equal. apply (plus_0_r n').
Qed.

Reset plus_0_r.

Version directe

Fixpoint plus_0_r n : n + 0 = n :=
  match n with
  | 0 ⇒ eq_refl
  | S n' ⇒ S_equal (n' + 0) n' (plus_0_r n')
  end.

Reset plus_0_r.

Remarque : écriture allégée, c.f. cours 5 à venir

Fixpoint plus_0_r n : n + 0 = n :=
  match n with
  | 0 ⇒ eq_refl
  | S n' ⇒ S_equal _ _ (plus_0_r n')
  end.

Même technique sur eq_eqnatb. Observation importante : Le programme récursif suit le même schéma que eqnatb

Fixpoint eq_eqnatb n1 n2 : eqnatb n1 n2 = true → n1 = n2 :=
  match n1,n2 with
  | O, O ⇒ fun e ⇒ eq_refl
  | S n1', S n2' ⇒ fun e ⇒ S_equal n1' n2' (eq_eqnatb n1' n2' e)
  | x, y ⇒ fun e ⇒ false_true_eg e x y
  end.

Observer que le type de e, dans le cas récursif, est à la fois (eqnatb (S n1') (S n2') = true et eqnatb n1' n2' = true qui sont des expressions interchangeables car convertibles par calcul. Cea apparaît mieux lors de la mise au point avec refine

Reset eq_eqnatb.
Fixpoint eq_eqnatb n1 n2 : eqnatb n1 n2 = true → n1 = n2.
  refine (
  match n1,n2 with
  | O, O ⇒ fun e ⇒ _
  | S n1', S n2' ⇒ fun e ⇒ _
  | x, y ⇒ fun e ⇒ _
  end).

Compléter

Admitted.

Dans la même veine, revoir et expliquer la manière dont la correction de la fonction simpl0 du TD2 a été prouvée