some_neg

A special some predicate for lists

some_neg asserts that some element of a list l fulfills a predicate P, with the twist that it asserts P for singleton lists and ~~P if the length of l is different than 1.

some_neg corresponds precisely to the semantics of sequents. For sequents with more than one formula, the formulas are or-ed, but because disjunction is not in the object logic, ¬ (~ _ ∧ ¬ _) is used. This leads to the double negation for sequents with more than one formula.

I first define the dependent version some_neg_dep. Dependent here means that the predicate P can only be applied when a certain condition is true. some_neg_dep gets this condition for the whole list in the form of an every_nth predicate.

The simple independent version and all its results are directly derived from the dependent version.

Require Export reorder.

Dependent version

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

  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.

Introduction and Elimination

  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.

Append Properties

  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.

Reorder Properties

  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.

Simple, independent version

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].