Commit 838fbc06 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

TD2 : solutions for extra proofs about <=

parent 5d3f730e
......@@ -175,22 +175,37 @@ Qed.
Lemma le_succ : forall n m, n <= m -> n <= S m.
Proof.
Admitted.
intros n m (q,H). exists (S q). rewrite add_succ_r. f_equal. apply H.
Qed.
Lemma le_total : forall n m, n <= m \/ m <= n.
Proof.
Admitted.
induction n.
- left; exists m; auto.
- destruct m.
+ right; exists (S n); auto.
+ destruct (IHn m).
* left. destruct H as (q,H). exists q. simpl. f_equal. assumption.
* right. destruct H as (q,H). exists q. simpl. f_equal. assumption.
Qed.
Close Scope alt_le_scope.
Locate "<=". (* Now <= is back to the default definition of Coq *)
Print Peano.le. (* The one of Coq : an inductive definition *)
Lemma coq_le_add_r : forall n m, n <= n+m.
Proof.
induction m.
- rewrite add_0_r. apply Peano.le_n.
- rewrite add_succ_r. apply Peano.le_S. assumption.
Qed.
Lemma le_equiv : forall n m, n <= m <-> le n m.
Proof.
split.
- intros H; induction H. (* induction on a inductive proof ! *)
+ admit. (* TODO *)
+ admit. (* TODO *)
- admit. (* TODO *)
Admitted.
+ apply le_refl.
+ apply le_succ; assumption.
- intros (q,H). rewrite <- H. apply coq_le_add_r.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment