A special some predicate for lists
Section Some_neg_dep.
Variable A : Type.
Variable aprop : A → Prop.
Variable P : ∀(a : A), aprop a → Prop.
Hypothesis P_tcc_irr : ∀(a : A)(ta1 ta2 : aprop a),
P a ta1 → P a ta2.
Definition a_list_prop(l : list A) : Prop :=
every_nth aprop l.
Definition some_neg_dep(l : list A)(dep : a_list_prop l) : Prop :=
(len # length l = 1 /#\
P (nth l 0 (nth_head_tcc l len)) (dep 0 (nth_head_tcc l len)))
∨
(length l ≠ 1 ∧
¬ ¬ ∃(n : nat),
n_less # n < length l /#\ P (nth l n n_less) (dep n n_less)).
Lemma some_neg_dep_tcc_irr : ∀(l : list A)(dep1 dep2 : a_list_prop l),
some_neg_dep l dep1 → some_neg_dep l dep2.
Lemma some_neg_dep_empty : ∀(dep : a_list_prop []),
some_neg_dep [] dep → False.
Lemma some_neg_dep_singleton : ∀(a : A)(dep : a_list_prop [a]),
some_neg_dep [a] dep → P a (dep 0 (lt_0_Sn 0)).
Lemma some_neg_dep_singleton_rev :
∀(a : A)(dep : a_list_prop [a])(ta : aprop a),
P a ta → some_neg_dep [a] dep.
Lemma some_neg_dep_nth_intro :
∀(l : list A)(dep : a_list_prop l)
(n : nat)(n_less : n < length l)(tn : aprop (nth l n n_less)),
P (nth l n n_less) tn → some_neg_dep l dep.
Definition a_list_prop_head :
∀{a : A}{l : list A}, a_list_prop (a :: l) → aprop a :=
fun _ l dep ⇒ dep 0 (lt_0_Sn (length l)).
Lemma a_list_prop_tail :
∀{a : A}{l : list A}, a_list_prop (a :: l) → a_list_prop l.
Lemma some_neg_dep_cons_case_elim :
∀(a : A)(l : list A)(dep : a_list_prop (a :: l)),
some_neg_dep (a :: l) dep →
((l = [] ∧ P a (a_list_prop_head dep)) ∨
(l ≠ [] ∧ ~(~P a (a_list_prop_head dep) ∧
¬some_neg_dep l (a_list_prop_tail dep)))).
Lemma some_neg_dep_cons_cons_elim :
∀(a a' : A)(l : list A)(dep : a_list_prop (a :: a' :: l)),
some_neg_dep (a :: a' :: l) dep →
~(~P a (a_list_prop_head dep) ∧
¬some_neg_dep (a' :: l) (a_list_prop_tail dep)).
Lemma some_neg_dep_head :
∀(a : A)(t0 : aprop a)(l : list A)(dep : a_list_prop (a :: l)),
P a t0 → some_neg_dep (a :: l) dep.
some_neg_dep_tail is further below
Lemma some_neg_dep_length_case_intro :
∀(l : list A)(dep : a_list_prop l),
(∀(len : length l = 1),
P (nth l 0 (nth_head_tcc l len)) (dep 0 (nth_head_tcc l len))) →
(length l ≠ 1 → ~~some_neg_dep l dep) →
some_neg_dep l dep.
Lemma some_neg_dep_cons_case_intro :
∀(a : A)(l : list A)(dep : a_list_prop (a :: l)),
(l = [] → P a (a_list_prop_head dep)) →
(l ≠ [] → ~~some_neg_dep (a :: l) dep) →
some_neg_dep (a :: l) dep.
Lemma some_neg_dep_long_neg_intro : ∀(l : list A)(dep : a_list_prop l),
length l ≠ 1 → ~~some_neg_dep l dep → some_neg_dep l dep.
Lemma dep_append_left :
∀{l1 l2 : list A}, a_list_prop (l1 ++ l2) → a_list_prop l1.
Lemma dep_append_right :
∀{l1 l2 : list A}, a_list_prop (l1 ++ l2) → a_list_prop l2.
Lemma some_neg_dep_append :
∀(l1 l2 : list A)(dep : a_list_prop (l1 ++ l2)),
some_neg_dep (l1 ++ l2) dep →
¬ ( ¬ (some_neg_dep l1 (dep_append_left dep)) ∧
¬ (some_neg_dep l2 (dep_append_right dep))).
Lemma some_neg_dep_append_right :
∀(l1 l2 : list A)(dep : a_list_prop (l1 ++ l2)),
some_neg_dep l1 (dep_append_left dep) → some_neg_dep (l1 ++ l2) dep.
Lemma some_neg_dep_append_left :
∀(l1 l2 : list A)(dep : a_list_prop (l1 ++ l2)),
some_neg_dep l2 (dep_append_right dep) → some_neg_dep (l1 ++ l2) dep.
Lemma some_neg_dep_tail :
∀(a : A)(l : list A)(dep : a_list_prop (a :: l)),
some_neg_dep l (a_list_prop_tail dep) → some_neg_dep (a :: l) dep.
Lemma some_neg_dep_reorder :
∀(l1 l2 : list A)(dep1 : a_list_prop l1)(dep2 : a_list_prop l2),
list_reorder l1 l2 →
some_neg_dep l1 dep1 →
some_neg_dep l2 dep2.
End Some_neg_dep.
Implicit Arguments a_list_prop [A].
Implicit Arguments some_neg_dep [A].
Implicit Arguments a_list_prop_head [aprop A a l].
Implicit Arguments a_list_prop_tail [aprop A a l].
Lemma some_neg_dep_map :
∀{A B : Type}(f : A → B)(aprop : A → Prop)(bprop : B → Prop)
(prop_fun : ∀(a : A), aprop a → bprop (f a))
(P : ∀(b : B), bprop b → Prop)(l : list A)
(adep : a_list_prop aprop l)(bdep : a_list_prop bprop (map f l)),
(∀ (b : B) (tb1 tb2 : bprop b), P b tb1 → P b tb2) →
some_neg_dep aprop
(fun(a : A)(ap : aprop a) ⇒ P (f a) (prop_fun a ap)) l adep →
some_neg_dep bprop P (map f l) bdep.
Section Some_neg.
Variable A : Type.
Variable P : A → Prop.
Definition noprop(a : A) : Prop := True.
Definition lift_p : ∀(a : A), noprop a → Prop := fun a _ ⇒ P a.
Lemma lift_p_tcc_irr : ∀(a : A)(ta1 ta2 : noprop a),
lift_p a ta1 → lift_p a ta2.
Definition list_noprop(l : list A) : a_list_prop noprop l := fun _ _ ⇒ I.
Definition some_neg(l : list A) : Prop :=
some_neg_dep noprop lift_p l (list_noprop _).
All properties are phrased as definitions in the following,
because their proof simply uses the dependent proof with some
additional arguments.
Definition some_neg_empty :
some_neg [] → False :=
some_neg_dep_empty A noprop lift_p (list_noprop _).
Definition some_neg_singleton_for :
∀(a : A), some_neg [a] → P a :=
fun a ⇒ some_neg_dep_singleton
A noprop lift_p lift_p_tcc_irr a (list_noprop _).
Definition some_neg_singleton_back :
∀(a : A), P a → some_neg [a] :=
fun a ⇒ some_neg_dep_singleton_rev
A noprop lift_p lift_p_tcc_irr a (list_noprop _) I.
Lemma some_neg_singleton : ∀(a : A),
some_neg [a] ↔ P a.
Definition some_neg_nth_intro :
∀(l : list A)(n : nat)(n_less : n < length l),
P (nth l n n_less) → some_neg l :=
fun l n n_less ⇒ some_neg_dep_nth_intro
A noprop lift_p lift_p_tcc_irr l (list_noprop _) n n_less I.
Definition some_neg_cons_case_elim :
∀(a : A)(l : list A),
some_neg (a :: l) →
((l = [] ∧ P a) ∨
(l ≠ [] ∧ ~(~P a ∧ ¬some_neg l))) :=
fun a l ⇒ some_neg_dep_cons_case_elim
A noprop lift_p lift_p_tcc_irr a l (list_noprop _).
Definition some_neg_head :
∀(a : A)(l : list A), P a → some_neg (a :: l) :=
fun a l ⇒ some_neg_dep_head
A noprop lift_p lift_p_tcc_irr a I l (list_noprop _).
Definition some_neg_length_case_intro :
∀(l : list A),
(∀(len : length l = 1), P (nth l 0 (nth_head_tcc l len))) →
(length l ≠ 1 → ~~some_neg l) →
some_neg l :=
fun l ⇒ some_neg_dep_length_case_intro A noprop lift_p l (list_noprop _).
Definition some_neg_cons_case_intro :
∀(a : A)(l : list A),
(l = [] → P a) →
(l ≠ [] → ~~some_neg (a :: l)) →
some_neg (a :: l) :=
fun a l ⇒ some_neg_dep_cons_case_intro
A noprop lift_p lift_p_tcc_irr a l (list_noprop _).
Definition some_neg_long_neg_intro :
∀(l : list A), length l ≠ 1 → ~~some_neg l → some_neg l :=
fun l ⇒ some_neg_dep_long_neg_intro A noprop lift_p l (list_noprop _).
Definition some_neg_append :
∀(l1 l2 : list A),
some_neg (l1 ++ l2) → ¬ ( ¬ (some_neg l1) ∧ ¬ (some_neg l2)) :=
fun l1 l2 ⇒ some_neg_dep_append
A noprop lift_p lift_p_tcc_irr l1 l2 (list_noprop _).
Definition some_neg_append_right :
∀(l1 l2 : list A), some_neg l1 → some_neg (l1 ++ l2) :=
fun l1 l2 ⇒ some_neg_dep_append_right
A noprop lift_p lift_p_tcc_irr l1 l2 (list_noprop _).
Definition some_neg_append_left :
∀(l1 l2 : list A), some_neg l2 → some_neg (l1 ++ l2) :=
fun l1 l2 ⇒ some_neg_dep_append_left
A noprop lift_p lift_p_tcc_irr l1 l2 (list_noprop _).
Definition some_neg_tail :
∀(a : A)(l : list A), some_neg l → some_neg (a :: l) :=
fun a l ⇒ some_neg_dep_tail
A noprop lift_p lift_p_tcc_irr a l (list_noprop _).
Definition some_neg_reorder :
∀(l1 l2 : list A), list_reorder l1 l2 → some_neg l1 → some_neg l2 :=
fun l1 l2 ⇒ some_neg_dep_reorder
A noprop lift_p lift_p_tcc_irr l1 l2 (list_noprop _) (list_noprop _).
End Some_neg.
Implicit Arguments some_neg [A].