J'ai commencé à peine 1 semaine avec Coq. Je dois établir des preuves pour prouver l'équivalence deux notions.
1 2 3 4 5
| Inductive sorted_i : list nat -> Prop :=
sorted_i_nil : sorted_i nil
| sorted_i_cons : forall (a : nat) (l : list nat),
(forall b : nat, In b l -> a <= b) ->
sorted_i l -> sorted_i (a :: l) |
et
1 2 3 4 5 6
| sorted_d =
fun l : list nat =>
forall i j : nat,
i < j ->
forall a b : nat, nth_error l i = Some a -> nth_error l j = Some b -> a <= b
: list nat -> Prop |
Donc je dois montrer un Lemme qui est :
Lemma sortedEq : forall l, sorted_i l <-> sorted_d l.
J'ai commencé par :
pour découper l'équivalence, et puis monter les introductions.
Mais ensuite, je me suis bloqué car je n'ai aucune idée pour quel tactique sur quel truc à applique.
J'ai essayé avec
Coq l'a monté comme un sorted_d : nat en haut et laisse en bas le corps de sorted_d.
Mais après, vraiment, je suis perdu. Quelqu'un pourrait me donner un coup de main?
Partager