C'est quand on part d'un cas particulier pour aller vers un cas général.

Exemple :

• Une liste vide est ordonnée.
• Une liste avec une valeur est ordonnée.
• Une liste de type n :: l avec m <= n alors m :: n :: l est ordonnée.

Inductive sorted : list Z -> Prop :=
  | sorted0 : sorted nil
  | sorted1 : forall z:Z, sorted (z :: nil)
  | sorted2 :
      forall (z1 z2:Z) (l:list Z),
        z1 <= z2 ->
        sorted (z2 :: l) -> sorted (z1 :: z2 :: l).

Université de Pennsylvanie Archive Logical Foundations v9.0.0 Programming Language Foundations v9.0.0 Verified Functional Algorithms v9.0.0 QuickChick: Property-Based Testing in Coq v9.0.0 Verifiable C v8.16 Separation Logic Foundations v9.0.0

Adam Chlipala Archive

Coq'Art en français. Archive

Coq'Art