From Equations Require Import Equations.

Section Syntaxe.

(*
1 : branchement simple:
  - On répète le nom de la fonction et on sépare par des ";".
  - On peut utiliser des underscores, comme dans un pattern matching classique.
  - Pas de end à la fin.
*)

Equations is0 (n : nat) : bool :=
  is0 0 => true;
  is0 _ => false.

(*
2 : Plusieurs branchements (là où on mettrait plusieurs match et/ou if then else):
  - Utiliser une clause with (nom de l'objet à match)
    puis mettre le nouveau branchement entre accolades
  - La clause with peut mentioner les arguments
  - Pour les nouvelles branches, c'est comme avant en considérant
    que la fonction a un nouvel argument (le nouvel objet sur lequel on branche)
*)

Equations pair (n : nat) : bool :=
  pair 0 => true;
  pair (S n) with pair n => {
    pair (S n) true => false; (* Mais pas besoin de repréciser le (S n) en fait: *)
    pair _ false => true
  }.

(*
3 : Syntaxe un peu plus simple pour les nouveau branchements :
    - Un peu plus proche de Rocq ("| ...") mais toujours pas de end
    - Uniquement si la valeur des autres arguments ne change plus
      (la plupart du temps le cas)
*)

Equations odd (n : nat) : bool :=
  odd (S n) with odd n => {
    | true => false
    | _ => true
  };
  odd _ => false.

(* Contre exemple (idiot) où on ne peut pas utiliser cette syntaxe: *)

Equations oddor0 (n : nat) : bool :=
  oddor0 n with pair n => {
    oddor0 0 _ => true;
    oddor0 _ true => false;
    oddor0 _ false => true;
  }.

End Syntaxe.

Section Preuve_de_décroissance.
(* Quand on définit une fonction avec "by wf" au lieu de récurrence structurelle comme rocq,
   il faut prouver que les appels récursifs décroissent bien. Deux méthodes:
   1 : Obligations, avec "Next Obligation. [...] Qed.". *)

Equations impossible (n : nat) : nat by wf n lt :=
  impossible n => impossible (S n) + impossible (S n).
Next Obligation.
  (* évidemment impossible *)
Admitted.
Next Obligation.
Admitted.

(*
   2 : Utiliser Equations? à la place ouvre directement une preuve avec
       un goal par appel récursif
*)

Axiom biensûr : forall n, S n < n.
Equations? impossible2 (n : nat) : nat by wf n lt :=
  impossible2 n => impossible2 (S n) * impossible2 (S n).
Proof. all: apply biensûr. Qed.

End Preuve_de_décroissance.

Section tactiques.
(* 2 tactiques à connaître:
   - funelim : pour raisonner par récurrence, avec une récurrence vraiment
     adaptée à votre fonction.
     syntaxe : "funelim ([appel de la fonction sur lequel raisonner])."
   - simp : pour simplifier les valeurs de la fonction.
     Ne fonctionne que si ça peut être simplifié.
     syntaxe : "simp [nom de la fonction]" *)
Lemma oddisnotpair n : odd n = negb (pair n).
Proof.
  funelim (pair n). (* c'est bien "(pair n)" et pas juste pair. *)
  (* Trois cas : exactement un par branche de la fonction ! *)
  - simp odd. reflexivity.
  - simp odd.
    (* ici simp ne fonctionne pas bien : odd n n'est pas calculable donc impossible
       de faire le calcul du branchement. Bon, le problème c'est qu'ici on a quand
       même envie de simplifier donc on peut l'aider, mais on ne rencontre pas de
       tel cas dans le projet. Remarquez qu'on ne simplifie jamais pair:
       funelim remplace déjà les occurences concernées par les bonnes valeurs. *)
    rewrite Hind,Heq. simpl. reflexivity.
  - now simp odd ; rewrite Hind,Heq.
Qed.

End tactiques.