Commit 48892265 authored by pa's avatar pa

Commit du desespoir

parent f9b8a35e
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require List.
Import List.ListNotations.
Open Scope list_scope.
Variable A : Type.
Axiom Implies : forall (P Q : Prop), (~ P -> Q) -> P \/ Q.
Fixpoint repeats (l : list A) : Prop :=
match l with
| [] => False
| t::q => List.In t q \/ repeats q
end.
Definition pigeon_predicat (l1 l2 : list A) := (forall (x : A), List.In x l1 -> List.In x l2) /\ List.length l1 > List.length l2.
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
Lemma taille_descendante (a : A) (l : list A)
: List.In a l -> List.length (List.remove eq_dec a l) < List.length l.
move : a.
elim : l . by rewrite /List.In.
move => a l HR x H. simpl.
Admitted.
Lemma ltn_leq_trans (n m p : nat) : n < m -> m <= p -> n < p.
Admitted.
Lemma first_lst (x a : A) (l : list A) : List.In x (a :: l) -> (a = x \/ List.In x l).
rewrite /List.In => //=.
Qed.
Lemma pigeon (l : list A) : (exists (l2 : list A), pigeon_predicat l l2) -> repeats l.
elim : l => //=. rewrite /pigeon_predicat. move => H.
destruct H. destruct H. by rewrite /length ltn0 in H0.
move => a l HR PP. destruct PP. rename x into l2.
rewrite /pigeon_predicat in H. destruct H. move : (H a). rewrite [in (_ a (a ::l))]/List.In.
move => H1. have : a=a \/ (fix In (a : A) (l : seq A) {struct l} : Prop :=
match l with
| [] => False
| (b :: m)%SEQ => b = a \/ In a m
end) a l . left. reflexivity. move => H2. have : List.In a l2. apply /(Basics.apply H1 H2).
clear H2 H1. move => H1.
assert (length (a::l) = length l + 1).
rewrite /length addn1 => //=. rewrite H2 in H0. rewrite addn1 ltnS in H0. clear H2.
rewrite /pigeon_predicat in HR.
remember (List.remove eq_dec a l2) as l3.
assert (List.length l3 < List.length l2). move : H1. rewrite Heql3. by apply taille_descendante.
assert (List.length l3 < List.length l). move : H2 H0. by apply ltn_leq_trans. clear H0 H2.
apply Implies. move => H0.
Admitted.
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