text:
Require Import Frap.

(* The following definition closely mirrors a standard BNF grammar for expressions.
 * It defines abstract syntax trees of arithmetic expressions. *)
Inductive arith : Set :=
| Const (n : nat)
| Plus (e1 e2 : arith)
| Times (e1 e2 : arith).

(* Here are a few examples of specific expressions. *)
Example ex1 := Const 42.
Example ex2 := Plus (Const 1) (Times (Const 2) (Const 3)).

(* How many nodes appear in the tree for an expression? *)
Fixpoint size (e : arith) : nat :=
  match e with
  | Const _ => 1
  | Plus e1 e2 => 1 + size e1 + size e2
  | Times e1 e2 => 1 + size e1 + size e2
  end.

(* Here's how to run a program (evaluate a term) in Coq. *)
Compute size ex1.
Compute size ex2.

(* What's the longest path from the root of a syntax tree to a leaf? *)
Fixpoint depth (e : arith) : nat :=
  match e with
  | Const _ => 1
  | Plus e1 e2 => 1 + max (depth e1) (depth e2)
  | Times e1 e2 => 1 + max (depth e1) (depth e2)
  end.

Compute depth ex1.
Compute depth ex2.

(* Our first proof!
 * Size is an upper bound on depth. *)
Theorem depth_le_size : forall e, depth e <= size e.
Proof.
Admitted.

(* A silly recursive function: swap the operand orders of all binary operators. *)
Fixpoint commuter (e : arith) : arith :=
  match e with
  | Const _ => e
  | Plus e1 e2 => Plus (commuter e2) (commuter e1)
  | Times e1 e2 => Times (commuter e2) (commuter e1)
  end.

Compute commuter ex1.
Compute commuter ex2.

(* [commuter] has all the appropriate interactions with other functions (and itself). *)

Theorem size_commuter : forall e, size (commuter e) = size e.
Proof.
Admitted.

Theorem depth_commuter : forall e, depth (commuter e) = depth e.
Proof.
Admitted.

Theorem commuter_inverse : forall e, commuter (commuter e) = e.
Proof.
Admitted.

(* Now we go back and add this constructor to [arith]:
   <<
  | Var (x : var)
   >>

(* Now that we have variables, we can consider new operations,
 * like substituting an expression for a variable. *)
Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
  match inThis with
  | Const _ => inThis
  | Var x => if x ==v replaceThis then withThis else inThis
  | Plus e1 e2 => Plus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
  | Times e1 e2 => Times (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
  end.

(* An intuitive property about how much [substitute] might increase depth. *)
Theorem substitute_depth : forall replaceThis withThis inThis,
  depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
Proof.
  admit.
Qed.

(* A silly self-substitution has no effect. *)
Theorem substitute_self : forall replaceThis inThis,
  substitute inThis replaceThis (Var replaceThis) = inThis.
Proof.
  admit.
Qed.

(* We can do substitution and commuting in either order. *)
Theorem substitute_commuter : forall replaceThis withThis inThis,
  commuter (substitute inThis replaceThis withThis)
  = substitute (commuter inThis) replaceThis (commuter withThis).
Proof.
  admit.
Qed.

(* *Constant folding* is one of the classic compiler optimizations.
 * We repeatedly find opportunities to replace fancier expressions
 * with known constant values. *)
Fixpoint constantFold (e : arith) : arith :=
  match e with
  | Const _ => e
  | Var _ => e
  | Plus e1 e2 =>
    let e1' := constantFold e1 in
    let e2' := constantFold e2 in
    match e1', e2' with
    | Const n1, Const n2 => Const (n1 + n2)
    | Const 0, _ => e2'
    | _, Const 0 => e1'
    | _, _ => Plus e1' e2'
    end
  | Times e1 e2 =>
    let e1' := constantFold e1 in
    let e2' := constantFold e2 in
    match e1', e2' with
    | Const n1, Const n2 => Const (n1 * n2)
    | Const 1, _ => e2'
    | _, Const 1 => e1'
    | Const 0, _ => Const 0
    | _, Const 0 => Const 0
    | _, _ => Times e1' e2'
    end
  end.

(* This is supposed to be an *optimization*, so it had better not *increase*
 * the size of an expression! *)
Theorem size_constantFold : forall e, size (constantFold e) <= size e.
Proof.
  admit.
Qed.

(* Business as usual, with another commuting law *)
Theorem commuter_constantFold : forall e, commuter (constantFold e) = constantFold (commuter e).
Proof.
  admit.
Qed.

(* To define a further transformation, we first write a roundabout way of
 * testing whether an expression is a constant. *)
Definition isConst (e : arith) : option nat :=
  match e with
  | Const n => Some n
  | _ => None
  end.

(* Our next target is a function that finds multiplications by constants
 * and pushes the multiplications to the leaves of syntax trees.
 * This helper function takes a coefficient [multiplyBy] that should be
 * applied to an expression. *)
Fixpoint pushMultiplicationInside' (multiplyBy : nat) (e : arith) : arith :=
  match e with
  | Const n => Const (multiplyBy * n)
  | Var _ => Times (Const multiplyBy) e
  | Plus e1 e2 => Plus (pushMultiplicationInside' multiplyBy e1)
                       (pushMultiplicationInside' multiplyBy e2)
  | Times e1 e2 =>
    match isConst e1 with
    | Some k => pushMultiplicationInside' (k * multiplyBy) e2
    | None => Times (pushMultiplicationInside' multiplyBy e1) e2
    end
  end.

(* The overall transformation just fixes the initial coefficient as [1]. *)
Definition pushMultiplicationInside (e : arith) : arith :=
  pushMultiplicationInside' 1 e.

(* Let's prove this boring arithmetic property, so that we may use it below. *)
Lemma n_times_0 : forall n, n * 0 = 0.
Proof.
  linear_arithmetic.
Qed.

(* A fun fact about pushing multiplication inside:
 * the coefficient has no effect on depth!
 * Let's show that any coefficient is equivalent to coefficient 0. *)
Lemma depth_pushMultiplicationInside'_irrelevance0 : forall e multiplyBy,
  depth (pushMultiplicationInside' multiplyBy e)
  = depth (pushMultiplicationInside' 0 e).
Proof.
  admit.
Qed.

(* Let's prove that pushing-inside has only a small effect on depth,
 * considering for now only coefficient 0. *)
Lemma depth_pushMultiplicationInside' : forall e,
  depth (pushMultiplicationInside' 0 e) <= S (depth e).
Proof.
  admit.
Qed.

Theorem depth_pushMultiplicationInside : forall e,
  depth (pushMultiplicationInside e) <= S (depth e).
Proof.
  admit.
Qed.
*)

author: achlipala

repo: frap

save_path: github-repos/coq/achlipala-frap


text:
Require Import Lia.
Require Import Bool.
Require Import RelationClasses.

From sflib Require Import sflib.
From Paco Require Import paco.

From PromisingLib Require Import Axioms.
From PromisingLib Require Import Basic.
From PromisingLib Require Import DataStructure.
From PromisingLib Require Import DenseOrder.
From PromisingLib Require Import Language.
From PromisingLib Require Import Loc.

From PromisingLib Require Import Event.
Require Import Time.

Require Import View.
Require Import Cell.
Require Import Memory.
Require Import TView.
Require Import Local.
Require Import Thread.

Require Import Cover.
Require Import Mapping.
Require Import Pred.
Require Import Trace.
Require Import MemoryProps.
Require Import PFConsistent.
Require Import CapFlex.
Require Import PFConsistentStrong.

Set Implicit Arguments.

Module FutureCertify.
  Section FutureCertify.
    Variable (lang: language).

    Lemma future_memory_map
          mem mem_cap mem_future times
          (CAP: Memory.cap mem mem_cap)
          (FUTURE: Memory.future_weak mem mem_future)
          (CLOSED: Memory.closed mem):
      exists (f: Loc.t -> Time.t -> Time.t -> Prop),
        (<<IDENT: map_ident_in_memory f mem>>) /\
        (<<MAPLT: mapping_map_lt_iff f>>) /\
        (<<MEMORY: memory_map f mem_cap mem_future>>) /\
        (<<COMPLETE: forall loc to (IN: List.In to (times loc)),
            exists fto, (<<MAPPED: f loc to fto>>)>>).
    Proof.
      exploit (choice (fun loc f =>
                         (<<COMPLETE: forall to (IN: List.In to (Time.incr (Memory.max_ts loc mem)::(times loc))), exists fto, (<<MAPPED: f to fto>>)>>) /\
                         (<<SAME: forall ts (TS: Time.le ts (Memory.max_ts loc mem)), f ts ts>>) /\
                         (<<BOUND: forall to fto (MAPPED: f to fto) (TS: Time.lt (Memory.max_ts loc mem) to),
                             (Time.lt (Time.join (Memory.max_ts loc mem_future) (Memory.max_ts loc mem)) fto)>>) /\
                         (<<MAPLT: mapping_map_lt_iff_loc f>>))).
      { intros loc. hexploit shift_map_exists.
        - eapply Time.join_r.
        - eapply Time.incr_spec.
        - i. des. exists f. esplits; eauto.
          i. exploit BOUND; eauto. intros x. des. eapply x. }
      intros [f FSPEC]. exists f.
      assert (IDENT: map_ident_in_memory f mem).
      { ii. specialize (FSPEC loc). des. eauto. }
      splits; eauto.
      - ii. specialize (FSPEC loc). des.
        red in MAPLT. eapply MAPLT; eauto.
      - econs.
        + i. eapply Memory.cap_inv in GET; eauto. des; eauto.
          dup GET. destruct (classic (msg = Message.reserve)); auto.
          eapply Memory.future_weak_get1 in GET; eauto; ss. des.
          right. esplits; eauto.
          * specialize (FSPEC loc). des. eapply SAME.
            eapply Memory.max_ts_spec in GET0. des. auto.
          * eapply map_ident_in_memory_closed_message; eauto.
            inv CLOSED. eapply CLOSED0 in GET0. des. eauto.
        + i. specialize (FSPEC loc). des.
          exploit COMPLETE.
          { ss. left. auto. } i. des.
          exploit BOUND; eauto.
          { eapply Time.incr_spec. } intros x.
          left. esplits.
          * eapply MAPPED.
          * eapply Time.bot_spec.
          * eapply Memory.max_ts_spec in GET. des.
            etrans; eauto. etrans.
            { eapply Time.join_l. }
            { left. eapply x. }
          * eapply map_ident_in_memory_bot; eauto.
          * i. inv CLOSED. eapply memory_cap_covered; eauto.
      - ii. specialize (FSPEC loc). des. eapply COMPLETE; ss; eauto.
    Qed.

    Lemma cap_steps_current_steps
          th0 th1 mem1 sc1
          (LOCAL: Local.wf (Thread.local th0) (Thread.memory th0))
          (MEMORY: Memory.closed (Thread.memory th0))
          (SC: Memory.closed_timemap (Thread.sc th0) (Thread.memory th0))
          (CAP: Memory.cap (Thread.memory th0) mem1)
          (SC_MAX: Memory.max_concrete_timemap mem1 sc1)
          (STEPS: rtc (@Thread.tau_step lang)
                      (Thread.mk lang (Thread.state th0) (Thread.local th0) sc1 mem1)
                      th1)
          (CONSISTENT: Local.promise_consistent (Thread.local th1))
      :
        exists lc' sc' mem',
          (<<STEPS: rtc (@Thread.tau_step lang)
                        th0
                        (Thread.mk lang (Thread.state th1) lc' sc' mem')>>) /\
          (<<CONSISTENT: Local.promise_consistent lc'>>)
    .
    Proof.
      eapply pred_steps_thread_steps in STEPS.
      destruct th0, th1. ss.
      hexploit steps_map.
      { eapply ident_map_le. }
      { eapply ident_map_bot. }
      { eapply ident_map_eq. }
      { eapply ident_map_lt. }
      { i. eapply ident_map_mappable_evt. }
      { eapply STEPS. }
      { ss. }
      { ss. }
      { ss. }
      { eapply Local.cap_wf; eauto. }
      { eapply LOCAL. }
      { eauto. }
      { eapply Memory.cap_closed; eauto. }
      { eauto. }
      { eapply Memory.max_concrete_timemap_closed; eauto. }
      { eapply map_ident_in_memory_local; eauto; ss.
        eapply ident_map_lt_iff.
      }
      { econs.
        { i. destruct (classic (msg = Message.reserve)); auto. right.
          exists to, from, msg.
          eapply Memory.cap_inv in GET; eauto. des; ss. esplits; eauto.
          { refl. }
          { eapply ident_map_message. }
          { refl. }
        }
        { i. eapply CAP in GET. left. exists fto, ffrom, fto, ffrom. splits; ss.
          { refl. }
          { refl. }
          { i. econs; eauto. }
        }
      }
      { eapply mapping_map_lt_iff_collapsable_unwritable. eapply ident_map_lt_iff. }
      { eapply ident_map_timemap. }
      { eapply Memory.max_concrete_timemap_spec; eauto.
        eapply Memory.cap_closed_timemap; eauto. }
      { instantiate (1:=fun _ => True). ss. }
      i. des. esplits.
      { eapply rtc_implies; try apply STEP. i. inv H. inv TSTEP. econs; eauto. }
      { inv LOCAL0. eapply promise_consistent_mon; cycle 1; eauto.
        { refl. }
        eapply promise_consistent_map; eauto.
        { eapply ident_map_le; eauto. }
        { eapply ident_map_eq; eauto. }
      }
    Qed.

    Definition future_certify lang (e:Thread.t lang): Prop :=
      forall sc1 mem1
        (FUTURE: Memory.future_weak (Thread.memory e) mem1)
        (FUTURE: TimeMap.le (Thread.sc e) sc1)
        (WF: Local.wf (Thread.local e) mem1)
        (SC: Memory.closed_timemap sc1 mem1)
        (MEM: Memory.closed mem1),
        (<<FAILURE: Thread.steps_failure (Thread.mk lang (Thread.state e) (Thread.local e) sc1 mem1)>>) \/
        exists e2,
          (<<STEPS: rtc (@Thread.tau_step lang) (Thread.mk lang (Thread.state e) (Thread.local e) sc1 mem1) e2>>) /\
          (<<PROMISES: (Local.promises (Thread.local e2)) = Memory.bot>>).

    Lemma future_certify_exists
          e
          (LOCAL: Local.wf (Thread.local e) (Thread.memory e))
          (MEMORY: Memory.closed (Thread.memory e))
          (SC: Memory.closed_timemap (Thread.sc e) (Thread.memory e))
          (CONSISTENT: @Thread.consistent lang e):
      future_certify e.
    Proof.
      eapply consistent_no_sc_trace_consistent in CONSISTENT; eauto.
      ii. hexploit Memory.cap_exists.
      { eapply MEMORY. } i. des.
      exploit CONSISTENT; eauto. i. des.

      hexploit trace_times_list_exists. i. des.
      hexploit (future_memory_map times CAP FUTURE); eauto. i. des.

      destruct e2.
      hexploit trace_steps_map.
      { eapply mapping_map_lt_iff_map_le; eauto. }
      { eapply map_ident_in_memory_bot; eauto. }
      { eapply mapping_map_lt_iff_map_eq; eauto. }
      { eapply mapping_map_lt_iff_map_lt; eauto. }
      { eapply wf_time_mapped_mappable; eauto. }
      { eauto. }
      { eauto. }
      { eauto. }
      { eauto. }
      { eapply Local.cap_wf; eauto. }
      { eapply WF. }
      { eauto. }
      { eapply Memory.cap_closed; eauto. }
      { eapply Memory.closed_timemap_bot. inv MEM. auto. }
      { eapply Memory.cap_closed_timemap; eauto. }
      { eapply map_ident_in_memory_local; eauto. }
      { eauto. }
      { eapply mapping_map_lt_iff_collapsable_unwritable. eauto. }
      { eapply map_ident_concrete_closed_timemap; eauto.
        ii. eapply IDENT; eauto. inv CONCRETE.
        eapply Memory.max_ts_spec in GET. des; eauto.
      }
      { ii. eapply Time.bot_spec. }
      i. des.
      hexploit no_sc_any_sc_traced.
      { eapply STEPS0. }
      { eauto. }
      { eauto. }
      { eauto. }
      { eapply List.Forall_forall. ii.
        eapply list_Forall2_in in H; eauto. des.
        eapply List.Forall_forall in NOSC; eauto.
        destruct a, x. ss. inv EVENT; ss.
      }
      i. des.
      eapply List.Forall2_app_inv_l in TRACE0. des. subst.
      eapply Trace.steps_separate in STEPS1. des.
      eapply Trace.silent_steps_tau_steps in STEPS2; cycle 1.
      { eapply List.Forall_forall. i.
        eapply list_Forall2_in in H; eauto. des.
        eapply List.Forall_forall in IN; eauto.
        destruct a, x. ss. inv EVENT; ss.
      }
      red in TRACE. des; clarify.
      { right. esplits.
        { eauto. }
        { inv TRACE1. inv STEPS3; ss. inv LOCAL0.
          rewrite PROMISES in PROMISES0.
          eapply bot_promises_map in PROMISES0; eauto.
        }
      }
      { left. repeat red.
        inv TRACE1. inv H3. des.
        inv STEPS3. inv TR. inv STEPS1; ss.
        esplits.
        { eauto. }
        { replace pf with true in STEP; [eauto|].
          inv STEP; inv STEP0; ss. inv EVENT; ss.
        }
        { inv EVENT; ss. }
      }
    Qed.

    Lemma future_consistent
          e sc' mem'
          (LOCAL: Local.wf (Thread.local e) (Thread.memory e))
          (MEMORY: Memory.closed (Thread.memory e))
          (SC: Memory.closed_timemap (Thread.sc e) (Thread.memory e))
          (CONSISTENT: @Thread.consistent lang e)
          (SC_FUTURE: TimeMap.le (Thread.sc e) sc')
          (MEM_FUTURE: Memory.future_weak (Thread.memory e) mem')
          (LOCAL': Local.wf (Thread.local e) mem')
          (MEMORY': Memory.closed mem')
          (SC': Memory.closed_timemap sc' mem'):
      Thread.consistent (Thread.mk lang (Thread.state e) (Thread.local e) sc' mem').
    Proof.
      ii. ss.
      eapply future_certify_exists; try exact CONSISTENT; eauto.
      - etrans; eauto. eapply Memory.cap_future_weak; eauto.
      - eapply Local.cap_wf; eauto.
      - eapply Memory.cap_closed_timemap; eauto.
      - eapply Memory.cap_closed; eauto.
    Qed.
  End FutureCertify.

  Lemma undef_added_step lang pf e th0 th1
        loc to0 to1 from1
        (STEP: @Thread.step lang pf e th0 th1)
        (PROMISED: concrete_promised th0.(Thread.local).(Local.promises) loc to0)
        (TS: Time.lt to0 to1)
        (UNCH: unchangable th0.(Thread.memory) th0.(Thread.local).(Local.promises) loc to1 from1 Message.undef)
        (CONSISTENT: Local.promise_consistent th0.(Thread.local))
        (LOCALWF: Local.wf th0.(Thread.local) th0.(Thread.memory))
    :
    (<<FAILURE: Thread.steps_failure th0>>) \/
    (<<PROMISED: concrete_promised th1.(Thread.local).(Local.promises) loc to0>>).
  Proof.
    dup STEP. inv STEP.
    { right. red.
      inv STEP1; ss. inv LOCAL. inv PROMISED. inv PROMISE; ss.
      { eapply Memory.add_get1 in GET; eauto. econs; eauto. }
      { eapply Memory.split_get1 in GET; eauto. des. econs; eauto. }
      { eapply Memory.lower_get1 in GET; eauto. des. econs; eauto. inv MSG_LE; ss. }
      { dup GET. eapply Memory.remove_get1 in GET; eauto. des; clarify.
        { eapply Memory.remove_get0 in PROMISES. des. clarify. }
        { econs; eauto. }
      }
    }
    { inv STEP1; ss. inv LOCAL; ss.
      { right. eauto. }
      { inv LOCAL0. eauto. }
      { destruct (Loc.eq_dec loc0 loc).
        { subst. left. repeat red. esplits; [refl|..].
          { econs 2. instantiate (2:=ThreadEvent.racy_write loc to1 val ord).
            econs; eauto. econs. econs; eauto.
            inv PROMISED. inv UNCH. econs; eauto; ss.
            eapply CONSISTENT in GET; eauto. red.
            etrans; [|eauto]. eapply TimeFacts.le_lt_lt; [|eapply GET]; eauto.
            eapply LOCALWF.
          }
          { ss. }
        }
        { inv PROMISED. right. inv LOCAL0. ss. econs.
          { erewrite Memory.write_get_diff_promise; eauto. }
          { eauto. }
        }
      }
      { destruct (Loc.eq_dec loc0 loc).
        { subst. left. repeat red. esplits; [refl|..].
          { econs 2. instantiate (2:=ThreadEvent.racy_update loc to1 valr valw ordr ordw).
            econs; eauto. econs. econs; eauto.
            inv PROMISED. inv UNCH. econs; eauto; ss.
            eapply CONSISTENT in GET; eauto. red.
            etrans; [|eauto]. eapply TimeFacts.le_lt_lt; [|eapply GET]; eauto.
            eapply LOCALWF.
          }
          { ss. }
        }
        { inv PROMISED. right. inv LOCAL1. inv LOCAL2. ss. econs.
          { erewrite Memory.write_get_diff_promise; eauto. }
          { eauto. }
        }
      }
      { inv LOCAL0. eauto. }
      { inv LOCAL0. eauto. }
      { inv LOCAL0. eauto. }
      { destruct (Loc.eq_dec loc0 loc).
        { subst. left. repeat red. esplits; [refl|..].
          { econs 2. instantiate (2:=ThreadEvent.racy_write loc to1 val ord).
            econs; eauto. econs. econs; eauto.
            inv PROMISED. inv UNCH. econs; eauto; ss.
            eapply CONSISTENT in GET; eauto. red.
            etrans; [|eauto]. eapply TimeFacts.le_lt_lt; [|eapply GET]; eauto.
            eapply LOCALWF.
          }
          { ss. }
        }
        { inv PROMISED. right. inv LOCAL0. ss. econs.
          { erewrite Memory.write_na_get_diff_promise; eauto. }
          { eauto. }
        }
      }
      { inv LOCAL0. eauto. }
      { inv LOCAL0. eauto. }
      { left. repeat red. esplits; eauto. }
    }
  Qed.

  Lemma undef_added_steps lang th0 th1
        loc to0 to1 from1
        (STEPS: rtc (@Thread.tau_step lang) th0 th1)
        (PROMISED: concrete_promised th0.(Thread.local).(Local.promises) loc to0)
        (TS: Time.lt to0 to1)
        (UNCH: unchangable th0.(Thread.memory) th0.(Thread.local).(Local.promises) loc to1 from1 Message.undef)
        (CONSISTENT: Local.promise_consistent th1.(Thread.local))
        (LOCALWF: Local.wf th0.(Thread.local) th0.(Thread.memory))
        (MEMWF: Memory.closed th0.(Thread.memory))
        (SCWF: Memory.closed_timemap th0.(Thread.sc) th0.(Thread.memory))
    :
    (<<FAILURE: Thread.steps_failure th0>>) \/
    (<<PROMISED: concrete_promised th1.(Thread.local).(Local.promises) loc to0>>).
  Proof.
    revert PROMISED UNCH CONSISTENT LOCALWF MEMWF SCWF. induction STEPS; i.
    { right. eauto. }
    { inv H. inv TSTEP. hexploit Thread.step_future; eauto. i. des.
      hexploit PromiseConsistent.rtc_tau_step_promise_consistent; eauto. i.
      hexploit PromiseConsistent.step_promise_consistent; eauto. i.
      hexploit undef_added_step; eauto. i. des; eauto.
      eapply unchangable_increase in UNCH; eauto.
      hexploit IHSTEPS; eauto. i. des.
      { left. red in FAILURE. des. repeat red. esplits; [|eauto|eauto].
        econs 2; [|eauto]. econs; eauto. econs; eauto.
      }
      { eauto. }
    }
  Qed.

  Lemma undef_added_failure lang st lc sc0 mem0 sc1 mem1
        (CONSISTENT: Thread.consistent (Thread.mk lang st lc sc0 mem0))
        (MEMLE: Memory.future_weak mem0 mem1)
        (SCLE: TimeMap.le sc0 sc1)
        (LOCAL: Local.wf lc mem0)
        (MEM0: Memory.closed mem0)
        (SC0: Memory.closed_timemap sc0 mem0)
        (MEM1: Memory.closed mem1)
        (SC1: Memory.closed_timemap sc1 mem1)
        (LOCAL1: Local.wf lc mem1)
        loc from0 to0 msg from1 to1
        (GET0: Memory.get loc to0 lc.(Local.promises) = Some (from0, msg))
        (MSG: msg <> Message.reserve)

        (GET1: Memory.get loc to1 mem1 = Some (from1, Message.undef))
        (TS: Time.lt to0 to1)
        (NONE: Memory.get loc to1 mem0 = None)
    :
      Thread.steps_failure (Thread.mk _ st lc sc1 mem1).
  Proof.
    eapply future_certify_exists in CONSISTENT; eauto.
    exploit CONSISTENT; eauto. i. des; ss; auto.
    eapply undef_added_steps in STEPS; eauto; ss.
    { des; eauto. exfalso. rewrite PROMISES in PROMISED.
      inv PROMISED. erewrite Memory.bot_get in GET. ss.
    }
    { econs; eauto. }
    { econs; eauto.
      destruct (Memory.get loc to1 lc.(Local.promises)) as [[]|] eqn:EQ; auto.
      eapply LOCAL in EQ. clarify.
    }
    { eapply Local.bot_promise_consistent; eauto. }
  Qed.
End FutureCertify.

author: snu-sf

repo: promising-seq-coq


text:
Require Import List.
Require Import String.

Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Core.RelDec.
(*Require Import Injection. *)

Open Scope string_scope.
Import MonadNotation ListNotations.
Open Scope monad_scope.

Set Implicit Arguments.
Set Maximal Implicit Insertion.

Module FunNotation.

  Notation "f $ x" := (f x)
    (at level 99, x at level 99, right associativity, only parsing).

  Notation "'begin' e1 'end'" := ((e1))
    (at level 0, only parsing).

End FunNotation.
Import FunNotation.

(* Uncomment the following line after we drop Coq 8.8: *)
(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
Definition uncurry A B C (f:A -> B -> C) (x:A * B) : C := let (a,b) := x in f a b.

(* Uncomment the following line after we drop Coq 8.8: *)
(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
Definition curry  {A B C} (f : A * B -> C) (a : A) (b : B) : C := f (a, b).

Lemma uncurry_curry : forall A B C (f : A -> B -> C) a b,
    curry (uncurry f) a b = f a b.
Proof.
  unfold curry, uncurry.
  reflexivity.
Qed.

Lemma curry_uncurry : forall A B C (f : A * B -> C) ab,
    uncurry (curry f) ab = f ab.
Proof.
  unfold uncurry, curry.
  destruct ab.
  reflexivity.
Qed.

Fixpoint zip A B (xs:list A) (ys:list B) : list (A * B) :=
  match xs, ys with
  | [], _ => []
  | _, [] => []
  | x::xs, y::ys => (x,y)::zip xs ys
  end
.

Fixpoint unzip A B (xys:list (A * B)) : list A * list B :=
match xys with
| [] => ([], [])
| (x,y)::xys => let (xs,ys) := unzip xys in (x::xs,y::ys)
end.

Definition sum_tot {A} (x:A + A) : A := match x with inl a => a | inr a => a end.

Definition forEach A B (xs:list A) (f:A -> B) : list B := map f xs.

Definition lsingleton {A} (x:A) : list A := [x].

Definition firstf {A B C} (f:A->C) (xy:A*B) : C*B :=
let (x,y) := xy in (f x, y).

Definition secondf {A B C} (f:B->C) (xy:A*B) : A*C :=
let (x,y) := xy in (x, f y).

Fixpoint update {K V} {kRealDec:RelDec (@eq K)} x v l : list (K * V) :=
match l with
| [] => [(x,v)]
| (y,w)::l' => if eq_dec x y then (x,v)::l' else (y,w)::update x v l'
end.

Definition updateMany {K V} {kRealDec:RelDec (@eq K)}
  (ups:list (K * V)) (init:list (K * V)) : list (K * V) :=
    fold_right (uncurry update) init ups.

author: coq-community

repo: coq-ext-lib


text:
Require Export ProjectiveGeometry.Dev.basic_rank_space_list.

Ltac clear_ineg_rk :=
repeat match goal with
| H : rk _ >= _ |- _ => clear H
| H : rk _ <= _ |- _ => clear H
end.

Ltac clear_all_rk :=
repeat match goal with
| H : rk _ = _ |- _ => clear H
| H : rk _ >= _ |- _ => clear H
| H : rk _ <= _ |- _ => clear H
end.

Ltac equalize_pts :=
repeat match goal with
| H : rk (?X0 :: ?X1 :: nil) = 1 |- _ =>
          let HH := fresh in assert(HH := couple_rk2 X0 X1 H);clear H;rewrite HH
end.

Ltac eliminate_hyps :=
repeat match goal with
| H : rk ?X = _, H0 : rk ?X >= _ |- _ => clear H0
| H : rk ?X = _, H0 : rk ?X <= _ |- _ => clear H0
| H : rk ?X >= _, H0 : rk ?X >= _ |- _ => clear H
| H : rk ?X <= _, H0 : rk ?X <= _ |- _ => clear H
| H : rk ?X >= ?Y, H0 : rk ?X <= ?Y |- _ =>  let HH := fresh in assert(HH : rk X = Y) by (omega)
end.

Lemma le_S_sym : forall n m : nat,
n >= S m -> n >= m.
Proof.
intros.
intuition.
Qed.

Lemma eq_to_ge : forall n m : nat,
n = m -> n >= m.
Proof.
intros.
intuition.
Qed.

Lemma eq_to_le : forall n m : nat,
n = m -> n <= m.
Proof.
intros.
intuition.
Qed.

Ltac solve_hyps_max H H0 :=
solve[apply matroid1_b_useful;simpl;repeat constructor
|apply rk_upper_dim
|apply Nat.eq_le_incl;apply H
|apply Nat.eq_le_incl;apply eq_sym;apply H
|apply H0
|apply le_S;apply H0
|apply le_S;apply le_S;apply H0
|apply le_S;apply le_S;apply le_S;apply H0
].

Ltac solve_hyps_min H H0:=
solve[apply matroid1_b_useful2;simpl;repeat constructor
|apply matroid1_a
|apply Nat.eq_le_incl;apply H
|apply Nat.eq_le_incl;apply eq_sym;apply H
|apply H0
|apply le_S_sym;apply H0
|apply le_S_sym;apply le_S_sym;apply H0
|apply le_S_sym;apply le_S_sym;apply le_S_sym;apply H0
].

Lemma l1_scheme : forall P1 P2 : Point,
                  forall P3 P4 : Point,
                  forall P5 : Point,
                  rk (P1 :: P2 :: P5 :: nil) = 3 ->
                  rk (P1 :: P3 :: P5 :: nil) = 2 ->
                  rk (P2 :: P4 :: P5 :: nil) = 2 ->
                  rk (P3 :: P5 :: nil) = 2 ->
                  rk (P4 :: P5 :: nil) = 2  ->  rk (P3 :: P4 :: P5 :: nil) = 3.
Proof.
intros P1 P2 P3 P4 P5 HP1P2P5eq HP1P3P5eq HP2P4P5eq HP3P5eq HP4P5eq.

try clear HP1P2m;assert(HP1P2m : rk(P1 :: P2 :: nil) >= 2).
{
	try assert(HP5Mtmp : rk(P5 :: nil) <= 1) by (solve_hyps_max HP5eq HP5M).
	try assert(HP1P2P5mtmp : rk(P1 :: P2 :: P5 :: nil) >= 3) by (solve_hyps_min HP1P2P5eq HP1P2P5m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: P2 :: nil) (P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P5 :: nil) (P1 :: P2 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P5 :: nil) ((P1 :: P2 :: nil) ++ (P5 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P5mtmp;try rewrite HT2 in HP1P2P5mtmp.
	assert(HT := rule_2 (P1 :: P2 :: nil) (P5 :: nil) (nil) 3 0 1 HP1P2P5mtmp Hmtmp HP5Mtmp Hincl); apply HT.
}

try clear HP1P2P3P4P5m;assert(HP1P2P3P4P5m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P5m;assert(HP1P2P3P4P5m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 3).
{
	try assert(HP1P2P5mtmp : rk(P1 :: P2 :: P5 :: nil) >= 3) by (solve_hyps_min HP1P2P5eq HP1P2P5m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P5 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P5 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil) 3 3 HP1P2P5mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P5M;assert(HP1P2P3P4P5M : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) <= 3).
{
	try assert(HP1P3P5Mtmp : rk(P1 :: P3 :: P5 :: nil) <= 2) by (solve_hyps_max HP1P3P5eq HP1P3P5M).
	try assert(HP2P4P5Mtmp : rk(P2 :: P4 :: P5 :: nil) <= 2) by (solve_hyps_max HP2P4P5eq HP2P4P5M).
	try assert(HP5mtmp : rk(P5 :: nil) >= 1) by (solve_hyps_min HP5eq HP5m).
	assert(Hincl : incl (P5 :: nil) (list_inter (P1 :: P3 :: P5 :: nil) (P2 :: P4 :: P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: P5 :: nil) (P1 :: P3 :: P5 :: P2 :: P4 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P3 :: P5 :: P2 :: P4 :: P5 :: nil) ((P1 :: P3 :: P5 :: nil) ++ (P2 :: P4 :: P5 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P1 :: P3 :: P5 :: nil) (P2 :: P4 :: P5 :: nil) (P5 :: nil) 2 2 1 HP1P3P5Mtmp HP2P4P5Mtmp HP5mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP2P5m;assert(HP2P5m : rk(P2 :: P5 :: nil) >= 2).
{
	try assert(HP1Mtmp : rk(P1 :: nil) <= 1) by (solve_hyps_max HP1eq HP1M).
	try assert(HP1P2P5mtmp : rk(P1 :: P2 :: P5 :: nil) >= 3) by (solve_hyps_min HP1P2P5eq HP1P2P5m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: nil) (P2 :: P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P5 :: nil) (P1 :: P2 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P5 :: nil) ((P1 :: nil) ++ (P2 :: P5 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P5mtmp;try rewrite HT2 in HP1P2P5mtmp.
	assert(HT := rule_4 (P1 :: nil) (P2 :: P5 :: nil) (nil) 3 0 1 HP1P2P5mtmp Hmtmp HP1Mtmp Hincl); apply HT.
}

try clear HP2P3P4P5M;assert(HP2P3P4P5M : rk(P2 :: P3 :: P4 :: P5 :: nil) <= 3).
{
	try assert(HP3Mtmp : rk(P3 :: nil) <= 1) by (solve_hyps_max HP3eq HP3M).
	try assert(HP2P4P5Mtmp : rk(P2 :: P4 :: P5 :: nil) <= 2) by (solve_hyps_max HP2P4P5eq HP2P4P5M).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P3 :: nil) (P2 :: P4 :: P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P4 :: P5 :: nil) (P3 :: P2 :: P4 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P3 :: P2 :: P4 :: P5 :: nil) ((P3 :: nil) ++ (P2 :: P4 :: P5 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P3 :: nil) (P2 :: P4 :: P5 :: nil) (nil) 1 2 0 HP3Mtmp HP2P4P5Mtmp Hmtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP2P3P4P5m;assert(HP2P3P4P5m : rk(P2 :: P3 :: P4 :: P5 :: nil) >= 2).
{
	try assert(HP2P5mtmp : rk(P2 :: P5 :: nil) >= 2) by (solve_hyps_min HP2P5eq HP2P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P2 :: P5 :: nil) (P2 :: P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P5 :: nil) (P2 :: P3 :: P4 :: P5 :: nil) 2 2 HP2P5mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P4P5m;assert(HP2P3P4P5m : rk(P2 :: P3 :: P4 :: P5 :: nil) >= 3).
{
	try assert(HP1P3P5Mtmp : rk(P1 :: P3 :: P5 :: nil) <= 2) by (solve_hyps_max HP1P3P5eq HP1P3P5M).
	try assert(HP1P2P3P4P5mtmp : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 3) by (solve_hyps_min HP1P2P3P4P5eq HP1P2P3P4P5m).
	try assert(HP3P5mtmp : rk(P3 :: P5 :: nil) >= 2) by (solve_hyps_min HP3P5eq HP3P5m).
	assert(Hincl : incl (P3 :: P5 :: nil) (list_inter (P1 :: P3 :: P5 :: nil) (P2 :: P3 :: P4 :: P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: P5 :: nil) (P1 :: P3 :: P5 :: P2 :: P3 :: P4 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P3 :: P5 :: P2 :: P3 :: P4 :: P5 :: nil) ((P1 :: P3 :: P5 :: nil) ++ (P2 :: P3 :: P4 :: P5 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4P5mtmp;try rewrite HT2 in HP1P2P3P4P5mtmp.
	assert(HT := rule_4 (P1 :: P3 :: P5 :: nil) (P2 :: P3 :: P4 :: P5 :: nil) (P3 :: P5 :: nil) 3 2 2 HP1P2P3P4P5mtmp HP3P5mtmp HP1P3P5Mtmp Hincl); apply HT.
}

try clear HP3P4P5m;assert(HP3P4P5m : rk(P3 :: P4 :: P5 :: nil) >= 2).
{
	try assert(HP3P5mtmp : rk(P3 :: P5 :: nil) >= 2) by (solve_hyps_min HP3P5eq HP3P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P3 :: P5 :: nil) (P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P3 :: P5 :: nil) (P3 :: P4 :: P5 :: nil) 2 2 HP3P5mtmp Hcomp Hincl); apply HT.
}

try clear HP3P4P5m;assert(HP3P4P5m : rk(P3 :: P4 :: P5 :: nil) >= 3).
{
	try assert(HP2P4P5Mtmp : rk(P2 :: P4 :: P5 :: nil) <= 2) by (solve_hyps_max HP2P4P5eq HP2P4P5M).
	try assert(HP2P3P4P5mtmp : rk(P2 :: P3 :: P4 :: P5 :: nil) >= 3) by (solve_hyps_min HP2P3P4P5eq HP2P3P4P5m).
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hincl : incl (P4 :: P5 :: nil) (list_inter (P2 :: P4 :: P5 :: nil) (P3 :: P4 :: P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P4 :: P5 :: nil) (P2 :: P4 :: P5 :: P3 :: P4 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P4 :: P5 :: P3 :: P4 :: P5 :: nil) ((P2 :: P4 :: P5 :: nil) ++ (P3 :: P4 :: P5 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP2P3P4P5mtmp;try rewrite HT2 in HP2P3P4P5mtmp.
	assert(HT := rule_4 (P2 :: P4 :: P5 :: nil) (P3 :: P4 :: P5 :: nil) (P4 :: P5 :: nil) 3 2 2 HP2P3P4P5mtmp HP4P5mtmp HP2P4P5Mtmp Hincl); apply HT.
}

assert(rk(P3 :: P4 :: P5 ::  nil) <= 3) by (clear_ineg_rk;try omega;try apply rk_upper_dim;try solve[apply matroid1_b_useful;simpl;intuition]).
assert(rk(P3 :: P4 :: P5 ::  nil) >= 1) by (clear_ineg_rk;try omega;try solve[apply matroid1_b_useful2;simpl;intuition]).
omega.
Qed.

Lemma rABOo_scheme : forall P1 P2 : Point,
                     forall P3 P4 : Point,
                     rk (P1 :: P2 :: P3 :: P4 :: nil) >= 4 ->
                     forall P5 : Point,
                     rk (P3 :: P4 :: P5 :: nil) = 2 ->
                     rk (P3 :: P5 :: nil) = 2 -> rk (P1 :: P2 :: P3 :: P5 :: nil) >= 4.
Proof.
intros P1 P2 P3 P4 HP1P2P3P4m P5 HP3P4P5eq HP3P5eq.

try clear HP1P2P3m;assert(HP1P2P3m : rk(P1 :: P2 :: P3 :: nil) >= 3).
{
	try assert(HP4Mtmp : rk(P4 :: nil) <= 1) by (solve_hyps_max HP4eq HP4M).
	try assert(HP1P2P3P4mtmp : rk(P1 :: P2 :: P3 :: P4 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4eq HP1P2P3P4m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: P2 :: P3 :: nil) (P4 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: P4 :: nil) ((P1 :: P2 :: P3 :: nil) ++ (P4 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4mtmp;try rewrite HT2 in HP1P2P3P4mtmp.
	assert(HT := rule_2 (P1 :: P2 :: P3 :: nil) (P4 :: nil) (nil) 4 0 1 HP1P2P3P4mtmp Hmtmp HP4Mtmp Hincl); apply HT.
}

try clear HP2P3P4m;assert(HP2P3P4m : rk(P2 :: P3 :: P4 :: nil) >= 3).
{
	try assert(HP1Mtmp : rk(P1 :: nil) <= 1) by (solve_hyps_max HP1eq HP1M).
	try assert(HP1P2P3P4mtmp : rk(P1 :: P2 :: P3 :: P4 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4eq HP1P2P3P4m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: nil) (P2 :: P3 :: P4 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: P4 :: nil) ((P1 :: nil) ++ (P2 :: P3 :: P4 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4mtmp;try rewrite HT2 in HP1P2P3P4mtmp.
	assert(HT := rule_4 (P1 :: nil) (P2 :: P3 :: P4 :: nil) (nil) 4 0 1 HP1P2P3P4mtmp Hmtmp HP1Mtmp Hincl); apply HT.
}

try clear HP3P4m;assert(HP3P4m : rk(P3 :: P4 :: nil) >= 2).
{
	try assert(HP2Mtmp : rk(P2 :: nil) <= 1) by (solve_hyps_max HP2eq HP2M).
	try assert(HP2P3P4mtmp : rk(P2 :: P3 :: P4 :: nil) >= 3) by (solve_hyps_min HP2P3P4eq HP2P3P4m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P2 :: nil) (P3 :: P4 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P4 :: nil) (P2 :: P3 :: P4 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P3 :: P4 :: nil) ((P2 :: nil) ++ (P3 :: P4 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP2P3P4mtmp;try rewrite HT2 in HP2P3P4mtmp.
	assert(HT := rule_4 (P2 :: nil) (P3 :: P4 :: nil) (nil) 3 0 1 HP2P3P4mtmp Hmtmp HP2Mtmp Hincl); apply HT.
}

try clear HP1P2m;assert(HP1P2m : rk(P1 :: P2 :: nil) >= 2).
{
	try assert(HP3P4Mtmp : rk(P3 :: P4 :: nil) <= 2) by (solve_hyps_max HP3P4eq HP3P4M).
	try assert(HP1P2P3P4mtmp : rk(P1 :: P2 :: P3 :: P4 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4eq HP1P2P3P4m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: P2 :: nil) (P3 :: P4 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: P4 :: nil) ((P1 :: P2 :: nil) ++ (P3 :: P4 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4mtmp;try rewrite HT2 in HP1P2P3P4mtmp.
	assert(HT := rule_2 (P1 :: P2 :: nil) (P3 :: P4 :: nil) (nil) 4 0 2 HP1P2P3P4mtmp Hmtmp HP3P4Mtmp Hincl); apply HT.
}

try clear HP1P2P3P4P5m;assert(HP1P2P3P4P5m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P5m;assert(HP1P2P3P4P5m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 3).
{
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil) 3 3 HP1P2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P5m;assert(HP1P2P3P4P5m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 4).
{
	try assert(HP1P2P3P4mtmp : rk(P1 :: P2 :: P3 :: P4 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4eq HP1P2P3P4m).
	assert(Hcomp : 4 <= 4) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: nil) 4 4 HP1P2P3P4mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P5m;assert(HP1P2P3P5m : rk(P1 :: P2 :: P3 :: P5 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P5 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P5m;assert(HP1P2P3P5m : rk(P1 :: P2 :: P3 :: P5 :: nil) >= 3).
{
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P5 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P5 :: nil) 3 3 HP1P2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P5m;assert(HP1P2P3P5m : rk(P1 :: P2 :: P3 :: P5 :: nil) >= 4).
{
	try assert(HP3P4P5Mtmp : rk(P3 :: P4 :: P5 :: nil) <= 2) by (solve_hyps_max HP3P4P5eq HP3P4P5M).
	try assert(HP1P2P3P4P5mtmp : rk(P1 :: P2 :: P3 :: P4 :: P5 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4P5eq HP1P2P3P4P5m).
	try assert(HP3P5mtmp : rk(P3 :: P5 :: nil) >= 2) by (solve_hyps_min HP3P5eq HP3P5m).
	assert(Hincl : incl (P3 :: P5 :: nil) (list_inter (P1 :: P2 :: P3 :: P5 :: nil) (P3 :: P4 :: P5 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: P5 :: nil) (P1 :: P2 :: P3 :: P5 :: P3 :: P4 :: P5 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: P5 :: P3 :: P4 :: P5 :: nil) ((P1 :: P2 :: P3 :: P5 :: nil) ++ (P3 :: P4 :: P5 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4P5mtmp;try rewrite HT2 in HP1P2P3P4P5mtmp.
	assert(HT := rule_2 (P1 :: P2 :: P3 :: P5 :: nil) (P3 :: P4 :: P5 :: nil) (P3 :: P5 :: nil) 4 2 2 HP1P2P3P4P5mtmp HP3P5mtmp HP3P4P5Mtmp Hincl); apply HT.
}

assert(rk(P1 :: P2 :: P3 :: P5 ::  nil) <= 4) by (clear_ineg_rk;try omega;try apply rk_upper_dim;try solve[apply matroid1_b_useful;simpl;intuition]).
assert(rk(P1 :: P2 :: P3 :: P5 ::  nil) >= 1) by (clear_ineg_rk;try omega;try solve[apply matroid1_b_useful2;simpl;intuition]).
omega.
Qed.

Lemma rk_line_unification : forall P1 P2 P3,
                            rk(P1 :: P2 :: nil) = 2 -> rk(P1 :: P3 :: nil) = 2 ->
                            rk(P2 :: P3 :: nil) = 2 -> rk(P1 :: P2 :: P3 :: nil) <= 2 ->
                            rk(P1 :: P2 :: P3 :: nil) = 2.
Proof.
intros P1 P2 P3 HP1P2eq HP1P3eq HP2P3eq HP1P2P3eq.

try clear HP1P2P3m;assert(HP1P2P3m : rk(P1 :: P2 :: P3 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

assert(rk(P1 :: P2 :: P3 ::  nil) <= 3) by (clear_ineg_rk;try omega;try apply rk_upper_dim;try solve[apply matroid1_b_useful;simpl;intuition]).
assert(rk(P1 :: P2 :: P3 ::  nil) >= 1) by (clear_ineg_rk;try omega;try solve[apply matroid1_b_useful2;simpl;intuition]).
omega.
Qed.

Lemma Desargues : forall P1 P2 P3 P4 P5 P6 P7 P8 P9 P10,
rk(P1 :: P4 :: P7 :: nil) = 2 -> rk(P2 :: P5 :: P7 :: nil) = 2 -> rk(P3 :: P6 :: P7 :: nil) = 2 ->
rk(P4 :: P5 :: P6 :: nil) = 3 -> rk(P1 :: P2 :: P3 :: nil) = 3 ->
rk(P1 :: P2 :: P3 :: P4 :: nil) = 4 ->
rk(P4 :: P5 :: P10 :: nil) = 2 -> rk(P1 :: P2 :: P10 :: nil) = 2 ->
rk(P4 :: P6 :: P9 :: nil) = 2 -> rk(P1 :: P3 :: P9 :: nil) = 2 ->
rk(P5 :: P6 :: P8 :: nil) = 2 -> rk(P2 :: P3 :: P8 :: nil) = 2 ->
rk(P1 :: P4 :: nil) = 2 -> rk(P3 :: P6 :: nil) = 2 -> rk(P2 :: P5 :: nil) = 2 ->
rk (P8 :: P9 :: P10 :: nil) = 2.
Proof.
intros P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 HP1P4P7eq HP2P5P7eq HP3P6P7eq HP4P5P6eq HP1P2P3eq HP1P2P3P4eq HP4P5P10eq HP1P2P10eq HP4P6P9eq HP1P3P9eq HP5P6P8eq HP2P3P8eq HP1P4eq HP3P6eq HP2P5eq.

try clear HP1P2m;assert(HP1P2m : rk(P1 :: P2 :: nil) >= 2).
{
	try assert(HP3Mtmp : rk(P3 :: nil) <= 1) by (solve_hyps_max HP3eq HP3M).
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: P2 :: nil) (P3 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: nil) ((P1 :: P2 :: nil) ++ (P3 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3mtmp;try rewrite HT2 in HP1P2P3mtmp.
	assert(HT := rule_2 (P1 :: P2 :: nil) (P3 :: nil) (nil) 3 0 1 HP1P2P3mtmp Hmtmp HP3Mtmp Hincl); apply HT.
}

try clear HP1P2P3P8P10m;assert(HP1P2P3P8P10m : rk(P1 :: P2 :: P3 :: P8 :: P10 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P8 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P8 :: P10 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P8P10m;assert(HP1P2P3P8P10m : rk(P1 :: P2 :: P3 :: P8 :: P10 :: nil) >= 3).
{
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P8 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P8 :: P10 :: nil) 3 3 HP1P2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P8P10M;assert(HP1P2P3P8P10M : rk(P1 :: P2 :: P3 :: P8 :: P10 :: nil) <= 3).
{
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(HP1P2P10Mtmp : rk(P1 :: P2 :: P10 :: nil) <= 2) by (solve_hyps_max HP1P2P10eq HP1P2P10M).
	try assert(HP2mtmp : rk(P2 :: nil) >= 1) by (solve_hyps_min HP2eq HP2m).
	assert(Hincl : incl (P2 :: nil) (list_inter (P2 :: P3 :: P8 :: nil) (P1 :: P2 :: P10 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P8 :: P10 :: nil) (P2 :: P3 :: P8 :: P1 :: P2 :: P10 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P3 :: P8 :: P1 :: P2 :: P10 :: nil) ((P2 :: P3 :: P8 :: nil) ++ (P1 :: P2 :: P10 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P2 :: P3 :: P8 :: nil) (P1 :: P2 :: P10 :: nil) (P2 :: nil) 2 2 1 HP2P3P8Mtmp HP1P2P10Mtmp HP2mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP1P3m;assert(HP1P3m : rk(P1 :: P3 :: nil) >= 2).
{
	try assert(HP2Mtmp : rk(P2 :: nil) <= 1) by (solve_hyps_max HP2eq HP2M).
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P2 :: nil) (P1 :: P3 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: nil) (P2 :: P1 :: P3 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P1 :: P3 :: nil) ((P2 :: nil) ++ (P1 :: P3 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3mtmp;try rewrite HT2 in HP1P2P3mtmp.
	assert(HT := rule_4 (P2 :: nil) (P1 :: P3 :: nil) (nil) 3 0 1 HP1P2P3mtmp Hmtmp HP2Mtmp Hincl); apply HT.
}

try clear HP1P2P3P8P9P10m;assert(HP1P2P3P8P9P10m : rk(P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P8P9P10m;assert(HP1P2P3P8P9P10m : rk(P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) >= 3).
{
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) 3 3 HP1P2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P8P9P10M;assert(HP1P2P3P8P9P10M : rk(P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) <= 3).
{
	try assert(HP1P3P9Mtmp : rk(P1 :: P3 :: P9 :: nil) <= 2) by (solve_hyps_max HP1P3P9eq HP1P3P9M).
	try assert(HP1P2P3P8P10Mtmp : rk(P1 :: P2 :: P3 :: P8 :: P10 :: nil) <= 3) by (solve_hyps_max HP1P2P3P8P10eq HP1P2P3P8P10M).
	try assert(HP1P3mtmp : rk(P1 :: P3 :: nil) >= 2) by (solve_hyps_min HP1P3eq HP1P3m).
	assert(Hincl : incl (P1 :: P3 :: nil) (list_inter (P1 :: P3 :: P9 :: nil) (P1 :: P2 :: P3 :: P8 :: P10 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) (P1 :: P3 :: P9 :: P1 :: P2 :: P3 :: P8 :: P10 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P3 :: P9 :: P1 :: P2 :: P3 :: P8 :: P10 :: nil) ((P1 :: P3 :: P9 :: nil) ++ (P1 :: P2 :: P3 :: P8 :: P10 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P1 :: P3 :: P9 :: nil) (P1 :: P2 :: P3 :: P8 :: P10 :: nil) (P1 :: P3 :: nil) 2 3 2 HP1P3P9Mtmp HP1P2P3P8P10Mtmp HP1P3mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP4P5m;assert(HP4P5m : rk(P4 :: P5 :: nil) >= 2).
{
	try assert(HP6Mtmp : rk(P6 :: nil) <= 1) by (solve_hyps_max HP6eq HP6M).
	try assert(HP4P5P6mtmp : rk(P4 :: P5 :: P6 :: nil) >= 3) by (solve_hyps_min HP4P5P6eq HP4P5P6m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P4 :: P5 :: nil) (P6 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P6 :: nil) (P4 :: P5 :: P6 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P4 :: P5 :: P6 :: nil) ((P4 :: P5 :: nil) ++ (P6 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP4P5P6mtmp;try rewrite HT2 in HP4P5P6mtmp.
	assert(HT := rule_2 (P4 :: P5 :: nil) (P6 :: nil) (nil) 3 0 1 HP4P5P6mtmp Hmtmp HP6Mtmp Hincl); apply HT.
}

try clear HP4P5P6P8P9m;assert(HP4P5P6P8P9m : rk(P4 :: P5 :: P6 :: P8 :: P9 :: nil) >= 2).
{
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: nil) (P4 :: P5 :: P6 :: P8 :: P9 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: nil) (P4 :: P5 :: P6 :: P8 :: P9 :: nil) 2 2 HP4P5mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P6P8P9m;assert(HP4P5P6P8P9m : rk(P4 :: P5 :: P6 :: P8 :: P9 :: nil) >= 3).
{
	try assert(HP4P5P6mtmp : rk(P4 :: P5 :: P6 :: nil) >= 3) by (solve_hyps_min HP4P5P6eq HP4P5P6m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: P6 :: nil) (P4 :: P5 :: P6 :: P8 :: P9 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: P6 :: nil) (P4 :: P5 :: P6 :: P8 :: P9 :: nil) 3 3 HP4P5P6mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P6P8P9M;assert(HP4P5P6P8P9M : rk(P4 :: P5 :: P6 :: P8 :: P9 :: nil) <= 3).
{
	try assert(HP5P6P8Mtmp : rk(P5 :: P6 :: P8 :: nil) <= 2) by (solve_hyps_max HP5P6P8eq HP5P6P8M).
	try assert(HP4P6P9Mtmp : rk(P4 :: P6 :: P9 :: nil) <= 2) by (solve_hyps_max HP4P6P9eq HP4P6P9M).
	try assert(HP6mtmp : rk(P6 :: nil) >= 1) by (solve_hyps_min HP6eq HP6m).
	assert(Hincl : incl (P6 :: nil) (list_inter (P5 :: P6 :: P8 :: nil) (P4 :: P6 :: P9 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P6 :: P8 :: P9 :: nil) (P5 :: P6 :: P8 :: P4 :: P6 :: P9 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P5 :: P6 :: P8 :: P4 :: P6 :: P9 :: nil) ((P5 :: P6 :: P8 :: nil) ++ (P4 :: P6 :: P9 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P5 :: P6 :: P8 :: nil) (P4 :: P6 :: P9 :: nil) (P6 :: nil) 2 2 1 HP5P6P8Mtmp HP4P6P9Mtmp HP6mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP4P5P6P8M;assert(HP4P5P6P8M : rk(P4 :: P5 :: P6 :: P8 :: nil) <= 3).
{
	try assert(HP4Mtmp : rk(P4 :: nil) <= 1) by (solve_hyps_max HP4eq HP4M).
	try assert(HP5P6P8Mtmp : rk(P5 :: P6 :: P8 :: nil) <= 2) by (solve_hyps_max HP5P6P8eq HP5P6P8M).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P4 :: nil) (P5 :: P6 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P6 :: P8 :: nil) (P4 :: P5 :: P6 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P4 :: P5 :: P6 :: P8 :: nil) ((P4 :: nil) ++ (P5 :: P6 :: P8 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P4 :: nil) (P5 :: P6 :: P8 :: nil) (nil) 1 2 0 HP4Mtmp HP5P6P8Mtmp Hmtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP4P5P6P8m;assert(HP4P5P6P8m : rk(P4 :: P5 :: P6 :: P8 :: nil) >= 2).
{
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: nil) (P4 :: P5 :: P6 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: nil) (P4 :: P5 :: P6 :: P8 :: nil) 2 2 HP4P5mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P6P8m;assert(HP4P5P6P8m : rk(P4 :: P5 :: P6 :: P8 :: nil) >= 3).
{
	try assert(HP4P5P6mtmp : rk(P4 :: P5 :: P6 :: nil) >= 3) by (solve_hyps_min HP4P5P6eq HP4P5P6m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: P6 :: nil) (P4 :: P5 :: P6 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: P6 :: nil) (P4 :: P5 :: P6 :: P8 :: nil) 3 3 HP4P5P6mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P7m;assert(HP1P2P3P4P7m : rk(P1 :: P2 :: P3 :: P4 :: P7 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P7 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P7 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P7m;assert(HP1P2P3P4P7m : rk(P1 :: P2 :: P3 :: P4 :: P7 :: nil) >= 3).
{
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P4 :: P7 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P4 :: P7 :: nil) 3 3 HP1P2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P7m;assert(HP1P2P3P4P7m : rk(P1 :: P2 :: P3 :: P4 :: P7 :: nil) >= 4).
{
	try assert(HP1P2P3P4mtmp : rk(P1 :: P2 :: P3 :: P4 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4eq HP1P2P3P4m).
	assert(Hcomp : 4 <= 4) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: P7 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: P7 :: nil) 4 4 HP1P2P3P4mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3m;assert(HP2P3m : rk(P2 :: P3 :: nil) >= 2).
{
	try assert(HP1Mtmp : rk(P1 :: nil) <= 1) by (solve_hyps_max HP1eq HP1M).
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P1 :: nil) (P2 :: P3 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: nil) ((P1 :: nil) ++ (P2 :: P3 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3mtmp;try rewrite HT2 in HP1P2P3mtmp.
	assert(HT := rule_4 (P1 :: nil) (P2 :: P3 :: nil) (nil) 3 0 1 HP1P2P3mtmp Hmtmp HP1Mtmp Hincl); apply HT.
}

try clear HP2P3P7m;assert(HP2P3P7m : rk(P2 :: P3 :: P7 :: nil) >= 2).
{
	try assert(HP2P3mtmp : rk(P2 :: P3 :: nil) >= 2) by (solve_hyps_min HP2P3eq HP2P3m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: nil) (P2 :: P3 :: P7 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: nil) (P2 :: P3 :: P7 :: nil) 2 2 HP2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P7m;assert(HP2P3P7m : rk(P2 :: P3 :: P7 :: nil) >= 3).
{
	try assert(HP1P4P7Mtmp : rk(P1 :: P4 :: P7 :: nil) <= 2) by (solve_hyps_max HP1P4P7eq HP1P4P7M).
	try assert(HP1P2P3P4P7mtmp : rk(P1 :: P2 :: P3 :: P4 :: P7 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4P7eq HP1P2P3P4P7m).
	try assert(HP7mtmp : rk(P7 :: nil) >= 1) by (solve_hyps_min HP7eq HP7m).
	assert(Hincl : incl (P7 :: nil) (list_inter (P2 :: P3 :: P7 :: nil) (P1 :: P4 :: P7 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: P7 :: nil) (P2 :: P3 :: P7 :: P1 :: P4 :: P7 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P3 :: P7 :: P1 :: P4 :: P7 :: nil) ((P2 :: P3 :: P7 :: nil) ++ (P1 :: P4 :: P7 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4P7mtmp;try rewrite HT2 in HP1P2P3P4P7mtmp.
	assert(HT := rule_2 (P2 :: P3 :: P7 :: nil) (P1 :: P4 :: P7 :: nil) (P7 :: nil) 4 1 2 HP1P2P3P4P7mtmp HP7mtmp HP1P4P7Mtmp Hincl); apply HT.
}

try clear HP2P3P5P7P8m;assert(HP2P3P5P7P8m : rk(P2 :: P3 :: P5 :: P7 :: P8 :: nil) >= 2).
{
	try assert(HP2P3mtmp : rk(P2 :: P3 :: nil) >= 2) by (solve_hyps_min HP2P3eq HP2P3m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: nil) (P2 :: P3 :: P5 :: P7 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: nil) (P2 :: P3 :: P5 :: P7 :: P8 :: nil) 2 2 HP2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P5P7P8m;assert(HP2P3P5P7P8m : rk(P2 :: P3 :: P5 :: P7 :: P8 :: nil) >= 3).
{
	try assert(HP2P3P7mtmp : rk(P2 :: P3 :: P7 :: nil) >= 3) by (solve_hyps_min HP2P3P7eq HP2P3P7m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: P7 :: nil) (P2 :: P3 :: P5 :: P7 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: P7 :: nil) (P2 :: P3 :: P5 :: P7 :: P8 :: nil) 3 3 HP2P3P7mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P5P7P8M;assert(HP2P3P5P7P8M : rk(P2 :: P3 :: P5 :: P7 :: P8 :: nil) <= 3).
{
	try assert(HP2P5P7Mtmp : rk(P2 :: P5 :: P7 :: nil) <= 2) by (solve_hyps_max HP2P5P7eq HP2P5P7M).
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(HP2mtmp : rk(P2 :: nil) >= 1) by (solve_hyps_min HP2eq HP2m).
	assert(Hincl : incl (P2 :: nil) (list_inter (P2 :: P5 :: P7 :: nil) (P2 :: P3 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P5 :: P7 :: P8 :: nil) (P2 :: P5 :: P7 :: P2 :: P3 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P5 :: P7 :: P2 :: P3 :: P8 :: nil) ((P2 :: P5 :: P7 :: nil) ++ (P2 :: P3 :: P8 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P2 :: P5 :: P7 :: nil) (P2 :: P3 :: P8 :: nil) (P2 :: nil) 2 2 1 HP2P5P7Mtmp HP2P3P8Mtmp HP2mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP2P3P5P8m;assert(HP2P3P5P8m : rk(P2 :: P3 :: P5 :: P8 :: nil) >= 2).
{
	try assert(HP2P3mtmp : rk(P2 :: P3 :: nil) >= 2) by (solve_hyps_min HP2P3eq HP2P3m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: nil) (P2 :: P3 :: P5 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: nil) (P2 :: P3 :: P5 :: P8 :: nil) 2 2 HP2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P5P8M;assert(HP2P3P5P8M : rk(P2 :: P3 :: P5 :: P8 :: nil) <= 3).
{
	try assert(HP5Mtmp : rk(P5 :: nil) <= 1) by (solve_hyps_max HP5eq HP5M).
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P5 :: nil) (P2 :: P3 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P5 :: P8 :: nil) (P5 :: P2 :: P3 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P5 :: P2 :: P3 :: P8 :: nil) ((P5 :: nil) ++ (P2 :: P3 :: P8 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P5 :: nil) (P2 :: P3 :: P8 :: nil) (nil) 1 2 0 HP5Mtmp HP2P3P8Mtmp Hmtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP2P3P5P8m;assert(HP2P3P5P8m : rk(P2 :: P3 :: P5 :: P8 :: nil) >= 3).
{
	try assert(HP2P5P7Mtmp : rk(P2 :: P5 :: P7 :: nil) <= 2) by (solve_hyps_max HP2P5P7eq HP2P5P7M).
	try assert(HP2P3P5P7P8mtmp : rk(P2 :: P3 :: P5 :: P7 :: P8 :: nil) >= 3) by (solve_hyps_min HP2P3P5P7P8eq HP2P3P5P7P8m).
	try assert(HP2P5mtmp : rk(P2 :: P5 :: nil) >= 2) by (solve_hyps_min HP2P5eq HP2P5m).
	assert(Hincl : incl (P2 :: P5 :: nil) (list_inter (P2 :: P5 :: P7 :: nil) (P2 :: P3 :: P5 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P5 :: P7 :: P8 :: nil) (P2 :: P5 :: P7 :: P2 :: P3 :: P5 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P5 :: P7 :: P2 :: P3 :: P5 :: P8 :: nil) ((P2 :: P5 :: P7 :: nil) ++ (P2 :: P3 :: P5 :: P8 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP2P3P5P7P8mtmp;try rewrite HT2 in HP2P3P5P7P8mtmp.
	assert(HT := rule_4 (P2 :: P5 :: P7 :: nil) (P2 :: P3 :: P5 :: P8 :: nil) (P2 :: P5 :: nil) 3 2 2 HP2P3P5P7P8mtmp HP2P5mtmp HP2P5P7Mtmp Hincl); apply HT.
}

try clear HP5P8m;assert(HP5P8m : rk(P5 :: P8 :: nil) >= 2).
{
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(HP2P3P5P8mtmp : rk(P2 :: P3 :: P5 :: P8 :: nil) >= 3) by (solve_hyps_min HP2P3P5P8eq HP2P3P5P8m).
	try assert(HP8mtmp : rk(P8 :: nil) >= 1) by (solve_hyps_min HP8eq HP8m).
	assert(Hincl : incl (P8 :: nil) (list_inter (P2 :: P3 :: P8 :: nil) (P5 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P5 :: P8 :: nil) (P2 :: P3 :: P8 :: P5 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P3 :: P8 :: P5 :: P8 :: nil) ((P2 :: P3 :: P8 :: nil) ++ (P5 :: P8 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP2P3P5P8mtmp;try rewrite HT2 in HP2P3P5P8mtmp.
	assert(HT := rule_4 (P2 :: P3 :: P8 :: nil) (P5 :: P8 :: nil) (P8 :: nil) 3 1 2 HP2P3P5P8mtmp HP8mtmp HP2P3P8Mtmp Hincl); apply HT.
}

try clear HP4P5P8m;assert(HP4P5P8m : rk(P4 :: P5 :: P8 :: nil) >= 2).
{
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: nil) (P4 :: P5 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: nil) (P4 :: P5 :: P8 :: nil) 2 2 HP4P5mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P8m;assert(HP4P5P8m : rk(P4 :: P5 :: P8 :: nil) >= 3).
{
	try assert(HP5P6P8Mtmp : rk(P5 :: P6 :: P8 :: nil) <= 2) by (solve_hyps_max HP5P6P8eq HP5P6P8M).
	try assert(HP4P5P6P8mtmp : rk(P4 :: P5 :: P6 :: P8 :: nil) >= 3) by (solve_hyps_min HP4P5P6P8eq HP4P5P6P8m).
	try assert(HP5P8mtmp : rk(P5 :: P8 :: nil) >= 2) by (solve_hyps_min HP5P8eq HP5P8m).
	assert(Hincl : incl (P5 :: P8 :: nil) (list_inter (P4 :: P5 :: P8 :: nil) (P5 :: P6 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P6 :: P8 :: nil) (P4 :: P5 :: P8 :: P5 :: P6 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P4 :: P5 :: P8 :: P5 :: P6 :: P8 :: nil) ((P4 :: P5 :: P8 :: nil) ++ (P5 :: P6 :: P8 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP4P5P6P8mtmp;try rewrite HT2 in HP4P5P6P8mtmp.
	assert(HT := rule_2 (P4 :: P5 :: P8 :: nil) (P5 :: P6 :: P8 :: nil) (P5 :: P8 :: nil) 3 2 2 HP4P5P6P8mtmp HP5P8mtmp HP5P6P8Mtmp Hincl); apply HT.
}

try clear HP4P5P8P9m;assert(HP4P5P8P9m : rk(P4 :: P5 :: P8 :: P9 :: nil) >= 2).
{
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: nil) (P4 :: P5 :: P8 :: P9 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: nil) (P4 :: P5 :: P8 :: P9 :: nil) 2 2 HP4P5mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P8P9m;assert(HP4P5P8P9m : rk(P4 :: P5 :: P8 :: P9 :: nil) >= 3).
{
	try assert(HP4P5P8mtmp : rk(P4 :: P5 :: P8 :: nil) >= 3) by (solve_hyps_min HP4P5P8eq HP4P5P8m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: P8 :: nil) (P4 :: P5 :: P8 :: P9 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: P8 :: nil) (P4 :: P5 :: P8 :: P9 :: nil) 3 3 HP4P5P8mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P8P9M;assert(HP4P5P8P9M : rk(P4 :: P5 :: P8 :: P9 :: nil) <= 3).
{
	try assert(HP4P5P6P8P9Mtmp : rk(P4 :: P5 :: P6 :: P8 :: P9 :: nil) <= 3) by (solve_hyps_max HP4P5P6P8P9eq HP4P5P6P8P9M).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: P8 :: P9 :: nil) (P4 :: P5 :: P6 :: P8 :: P9 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_6 (P4 :: P5 :: P8 :: P9 :: nil) (P4 :: P5 :: P6 :: P8 :: P9 :: nil) 3 3 HP4P5P6P8P9Mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P8P9P10m;assert(HP4P5P8P9P10m : rk(P4 :: P5 :: P8 :: P9 :: P10 :: nil) >= 2).
{
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: nil) (P4 :: P5 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: nil) (P4 :: P5 :: P8 :: P9 :: P10 :: nil) 2 2 HP4P5mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P8P9P10m;assert(HP4P5P8P9P10m : rk(P4 :: P5 :: P8 :: P9 :: P10 :: nil) >= 3).
{
	try assert(HP4P5P8mtmp : rk(P4 :: P5 :: P8 :: nil) >= 3) by (solve_hyps_min HP4P5P8eq HP4P5P8m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P4 :: P5 :: P8 :: nil) (P4 :: P5 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P5 :: P8 :: nil) (P4 :: P5 :: P8 :: P9 :: P10 :: nil) 3 3 HP4P5P8mtmp Hcomp Hincl); apply HT.
}

try clear HP4P5P8P9P10M;assert(HP4P5P8P9P10M : rk(P4 :: P5 :: P8 :: P9 :: P10 :: nil) <= 3).
{
	try assert(HP4P5P8P9Mtmp : rk(P4 :: P5 :: P8 :: P9 :: nil) <= 3) by (solve_hyps_max HP4P5P8P9eq HP4P5P8P9M).
	try assert(HP4P5P10Mtmp : rk(P4 :: P5 :: P10 :: nil) <= 2) by (solve_hyps_max HP4P5P10eq HP4P5P10M).
	try assert(HP4P5mtmp : rk(P4 :: P5 :: nil) >= 2) by (solve_hyps_min HP4P5eq HP4P5m).
	assert(Hincl : incl (P4 :: P5 :: nil) (list_inter (P4 :: P5 :: P8 :: P9 :: nil) (P4 :: P5 :: P10 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P8 :: P9 :: P10 :: nil) (P4 :: P5 :: P8 :: P9 :: P4 :: P5 :: P10 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P4 :: P5 :: P8 :: P9 :: P4 :: P5 :: P10 :: nil) ((P4 :: P5 :: P8 :: P9 :: nil) ++ (P4 :: P5 :: P10 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P4 :: P5 :: P8 :: P9 :: nil) (P4 :: P5 :: P10 :: nil) (P4 :: P5 :: nil) 3 2 2 HP4P5P8P9Mtmp HP4P5P10Mtmp HP4P5mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP1P2P3P4P5P8P9P10m;assert(HP1P2P3P4P5P8P9P10m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) >= 2).
{
	try assert(HP1P2mtmp : rk(P1 :: P2 :: nil) >= 2) by (solve_hyps_min HP1P2eq HP1P2m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) 2 2 HP1P2mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P5P8P9P10m;assert(HP1P2P3P4P5P8P9P10m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) >= 3).
{
	try assert(HP1P2P3mtmp : rk(P1 :: P2 :: P3 :: nil) >= 3) by (solve_hyps_min HP1P2P3eq HP1P2P3m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) 3 3 HP1P2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP1P2P3P4P5P8P9P10m;assert(HP1P2P3P4P5P8P9P10m : rk(P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) >= 4).
{
	try assert(HP1P2P3P4mtmp : rk(P1 :: P2 :: P3 :: P4 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4eq HP1P2P3P4m).
	assert(Hcomp : 4 <= 4) by (repeat constructor).
	assert(Hincl : incl (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P1 :: P2 :: P3 :: P4 :: nil) (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) 4 4 HP1P2P3P4mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P6P7P8m;assert(HP2P3P6P7P8m : rk(P2 :: P3 :: P6 :: P7 :: P8 :: nil) >= 2).
{
	try assert(HP2P3mtmp : rk(P2 :: P3 :: nil) >= 2) by (solve_hyps_min HP2P3eq HP2P3m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: nil) (P2 :: P3 :: P6 :: P7 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: nil) (P2 :: P3 :: P6 :: P7 :: P8 :: nil) 2 2 HP2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P6P7P8m;assert(HP2P3P6P7P8m : rk(P2 :: P3 :: P6 :: P7 :: P8 :: nil) >= 3).
{
	try assert(HP2P3P7mtmp : rk(P2 :: P3 :: P7 :: nil) >= 3) by (solve_hyps_min HP2P3P7eq HP2P3P7m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: P7 :: nil) (P2 :: P3 :: P6 :: P7 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: P7 :: nil) (P2 :: P3 :: P6 :: P7 :: P8 :: nil) 3 3 HP2P3P7mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P6P7P8M;assert(HP2P3P6P7P8M : rk(P2 :: P3 :: P6 :: P7 :: P8 :: nil) <= 3).
{
	try assert(HP3P6P7Mtmp : rk(P3 :: P6 :: P7 :: nil) <= 2) by (solve_hyps_max HP3P6P7eq HP3P6P7M).
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(HP3mtmp : rk(P3 :: nil) >= 1) by (solve_hyps_min HP3eq HP3m).
	assert(Hincl : incl (P3 :: nil) (list_inter (P3 :: P6 :: P7 :: nil) (P2 :: P3 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P6 :: P7 :: P8 :: nil) (P3 :: P6 :: P7 :: P2 :: P3 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P3 :: P6 :: P7 :: P2 :: P3 :: P8 :: nil) ((P3 :: P6 :: P7 :: nil) ++ (P2 :: P3 :: P8 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P3 :: P6 :: P7 :: nil) (P2 :: P3 :: P8 :: nil) (P3 :: nil) 2 2 1 HP3P6P7Mtmp HP2P3P8Mtmp HP3mtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP2P3P6P8m;assert(HP2P3P6P8m : rk(P2 :: P3 :: P6 :: P8 :: nil) >= 2).
{
	try assert(HP2P3mtmp : rk(P2 :: P3 :: nil) >= 2) by (solve_hyps_min HP2P3eq HP2P3m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P2 :: P3 :: nil) (P2 :: P3 :: P6 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P2 :: P3 :: nil) (P2 :: P3 :: P6 :: P8 :: nil) 2 2 HP2P3mtmp Hcomp Hincl); apply HT.
}

try clear HP2P3P6P8M;assert(HP2P3P6P8M : rk(P2 :: P3 :: P6 :: P8 :: nil) <= 3).
{
	try assert(HP6Mtmp : rk(P6 :: nil) <= 1) by (solve_hyps_max HP6eq HP6M).
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P6 :: nil) (P2 :: P3 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P6 :: P8 :: nil) (P6 :: P2 :: P3 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P6 :: P2 :: P3 :: P8 :: nil) ((P6 :: nil) ++ (P2 :: P3 :: P8 :: nil))) by (clear_all_rk;my_inO).
	assert(HT := rule_1 (P6 :: nil) (P2 :: P3 :: P8 :: nil) (nil) 1 2 0 HP6Mtmp HP2P3P8Mtmp Hmtmp Hincl);
	rewrite <-HT2 in HT;try rewrite <-HT1 in HT;apply HT.
}

try clear HP2P3P6P8m;assert(HP2P3P6P8m : rk(P2 :: P3 :: P6 :: P8 :: nil) >= 3).
{
	try assert(HP3P6P7Mtmp : rk(P3 :: P6 :: P7 :: nil) <= 2) by (solve_hyps_max HP3P6P7eq HP3P6P7M).
	try assert(HP2P3P6P7P8mtmp : rk(P2 :: P3 :: P6 :: P7 :: P8 :: nil) >= 3) by (solve_hyps_min HP2P3P6P7P8eq HP2P3P6P7P8m).
	try assert(HP3P6mtmp : rk(P3 :: P6 :: nil) >= 2) by (solve_hyps_min HP3P6eq HP3P6m).
	assert(Hincl : incl (P3 :: P6 :: nil) (list_inter (P3 :: P6 :: P7 :: nil) (P2 :: P3 :: P6 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P6 :: P7 :: P8 :: nil) (P3 :: P6 :: P7 :: P2 :: P3 :: P6 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P3 :: P6 :: P7 :: P2 :: P3 :: P6 :: P8 :: nil) ((P3 :: P6 :: P7 :: nil) ++ (P2 :: P3 :: P6 :: P8 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP2P3P6P7P8mtmp;try rewrite HT2 in HP2P3P6P7P8mtmp.
	assert(HT := rule_4 (P3 :: P6 :: P7 :: nil) (P2 :: P3 :: P6 :: P8 :: nil) (P3 :: P6 :: nil) 3 2 2 HP2P3P6P7P8mtmp HP3P6mtmp HP3P6P7Mtmp Hincl); apply HT.
}

try clear HP6P8m;assert(HP6P8m : rk(P6 :: P8 :: nil) >= 2).
{
	try assert(HP2P3P8Mtmp : rk(P2 :: P3 :: P8 :: nil) <= 2) by (solve_hyps_max HP2P3P8eq HP2P3P8M).
	try assert(HP2P3P6P8mtmp : rk(P2 :: P3 :: P6 :: P8 :: nil) >= 3) by (solve_hyps_min HP2P3P6P8eq HP2P3P6P8m).
	try assert(HP8mtmp : rk(P8 :: nil) >= 1) by (solve_hyps_min HP8eq HP8m).
	assert(Hincl : incl (P8 :: nil) (list_inter (P2 :: P3 :: P8 :: nil) (P6 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P2 :: P3 :: P6 :: P8 :: nil) (P2 :: P3 :: P8 :: P6 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P2 :: P3 :: P8 :: P6 :: P8 :: nil) ((P2 :: P3 :: P8 :: nil) ++ (P6 :: P8 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP2P3P6P8mtmp;try rewrite HT2 in HP2P3P6P8mtmp.
	assert(HT := rule_4 (P2 :: P3 :: P8 :: nil) (P6 :: P8 :: nil) (P8 :: nil) 3 1 2 HP2P3P6P8mtmp HP8mtmp HP2P3P8Mtmp Hincl); apply HT.
}

try clear HP4P6m;assert(HP4P6m : rk(P4 :: P6 :: nil) >= 2).
{
	try assert(HP5Mtmp : rk(P5 :: nil) <= 1) by (solve_hyps_max HP5eq HP5M).
	try assert(HP4P5P6mtmp : rk(P4 :: P5 :: P6 :: nil) >= 3) by (solve_hyps_min HP4P5P6eq HP4P5P6m).
	try assert(Hmtmp : rk(nil) >= 0) by (solve_hyps_min Hnuleq Hm).
	assert(Hincl : incl (nil) (list_inter (P5 :: nil) (P4 :: P6 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P6 :: nil) (P5 :: P4 :: P6 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P5 :: P4 :: P6 :: nil) ((P5 :: nil) ++ (P4 :: P6 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP4P5P6mtmp;try rewrite HT2 in HP4P5P6mtmp.
	assert(HT := rule_4 (P5 :: nil) (P4 :: P6 :: nil) (nil) 3 0 1 HP4P5P6mtmp Hmtmp HP5Mtmp Hincl); apply HT.
}

try clear HP4P6P8m;assert(HP4P6P8m : rk(P4 :: P6 :: P8 :: nil) >= 2).
{
	try assert(HP4P6mtmp : rk(P4 :: P6 :: nil) >= 2) by (solve_hyps_min HP4P6eq HP4P6m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P6 :: nil) (P4 :: P6 :: P8 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P6 :: nil) (P4 :: P6 :: P8 :: nil) 2 2 HP4P6mtmp Hcomp Hincl); apply HT.
}

try clear HP4P6P8m;assert(HP4P6P8m : rk(P4 :: P6 :: P8 :: nil) >= 3).
{
	try assert(HP5P6P8Mtmp : rk(P5 :: P6 :: P8 :: nil) <= 2) by (solve_hyps_max HP5P6P8eq HP5P6P8M).
	try assert(HP4P5P6P8mtmp : rk(P4 :: P5 :: P6 :: P8 :: nil) >= 3) by (solve_hyps_min HP4P5P6P8eq HP4P5P6P8m).
	try assert(HP6P8mtmp : rk(P6 :: P8 :: nil) >= 2) by (solve_hyps_min HP6P8eq HP6P8m).
	assert(Hincl : incl (P6 :: P8 :: nil) (list_inter (P4 :: P6 :: P8 :: nil) (P5 :: P6 :: P8 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P5 :: P6 :: P8 :: nil) (P4 :: P6 :: P8 :: P5 :: P6 :: P8 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P4 :: P6 :: P8 :: P5 :: P6 :: P8 :: nil) ((P4 :: P6 :: P8 :: nil) ++ (P5 :: P6 :: P8 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP4P5P6P8mtmp;try rewrite HT2 in HP4P5P6P8mtmp.
	assert(HT := rule_2 (P4 :: P6 :: P8 :: nil) (P5 :: P6 :: P8 :: nil) (P6 :: P8 :: nil) 3 2 2 HP4P5P6P8mtmp HP6P8mtmp HP5P6P8Mtmp Hincl); apply HT.
}

try clear HP4P6P8P9P10m;assert(HP4P6P8P9P10m : rk(P4 :: P6 :: P8 :: P9 :: P10 :: nil) >= 2).
{
	try assert(HP4P6mtmp : rk(P4 :: P6 :: nil) >= 2) by (solve_hyps_min HP4P6eq HP4P6m).
	assert(Hcomp : 2 <= 2) by (repeat constructor).
	assert(Hincl : incl (P4 :: P6 :: nil) (P4 :: P6 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P6 :: nil) (P4 :: P6 :: P8 :: P9 :: P10 :: nil) 2 2 HP4P6mtmp Hcomp Hincl); apply HT.
}

try clear HP4P6P8P9P10m;assert(HP4P6P8P9P10m : rk(P4 :: P6 :: P8 :: P9 :: P10 :: nil) >= 3).
{
	try assert(HP4P6P8mtmp : rk(P4 :: P6 :: P8 :: nil) >= 3) by (solve_hyps_min HP4P6P8eq HP4P6P8m).
	assert(Hcomp : 3 <= 3) by (repeat constructor).
	assert(Hincl : incl (P4 :: P6 :: P8 :: nil) (P4 :: P6 :: P8 :: P9 :: P10 :: nil)) by (repeat clear_all_rk;my_inO).
	assert(HT := rule_5 (P4 :: P6 :: P8 :: nil) (P4 :: P6 :: P8 :: P9 :: P10 :: nil) 3 3 HP4P6P8mtmp Hcomp Hincl); apply HT.
}

try clear HP8P9P10m;assert(HP8P9P10m : rk(P8 :: P9 :: P10 :: nil) >= 2).
{
	try assert(HP4P6P9Mtmp : rk(P4 :: P6 :: P9 :: nil) <= 2) by (solve_hyps_max HP4P6P9eq HP4P6P9M).
	try assert(HP4P6P8P9P10mtmp : rk(P4 :: P6 :: P8 :: P9 :: P10 :: nil) >= 3) by (solve_hyps_min HP4P6P8P9P10eq HP4P6P8P9P10m).
	try assert(HP9mtmp : rk(P9 :: nil) >= 1) by (solve_hyps_min HP9eq HP9m).
	assert(Hincl : incl (P9 :: nil) (list_inter (P4 :: P6 :: P9 :: nil) (P8 :: P9 :: P10 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P4 :: P6 :: P8 :: P9 :: P10 :: nil) (P4 :: P6 :: P9 :: P8 :: P9 :: P10 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P4 :: P6 :: P9 :: P8 :: P9 :: P10 :: nil) ((P4 :: P6 :: P9 :: nil) ++ (P8 :: P9 :: P10 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP4P6P8P9P10mtmp;try rewrite HT2 in HP4P6P8P9P10mtmp.
	assert(HT := rule_4 (P4 :: P6 :: P9 :: nil) (P8 :: P9 :: P10 :: nil) (P9 :: nil) 3 1 2 HP4P6P8P9P10mtmp HP9mtmp HP4P6P9Mtmp Hincl); apply HT.
}

try clear HP8P9P10M;assert(HP8P9P10M : rk(P8 :: P9 :: P10 :: nil) <= 2).
{
	try assert(HP1P2P3P8P9P10Mtmp : rk(P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) <= 3) by (solve_hyps_max HP1P2P3P8P9P10eq HP1P2P3P8P9P10M).
	try assert(HP4P5P8P9P10Mtmp : rk(P4 :: P5 :: P8 :: P9 :: P10 :: nil) <= 3) by (solve_hyps_max HP4P5P8P9P10eq HP4P5P8P9P10M).
	try assert(HP1P2P3P4P5P8P9P10mtmp : rk(P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) >= 4) by (solve_hyps_min HP1P2P3P4P5P8P9P10eq HP1P2P3P4P5P8P9P10m).
	assert(Hincl : incl (P8 :: P9 :: P10 :: nil) (list_inter (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) (P4 :: P5 :: P8 :: P9 :: P10 :: nil))) by (repeat clear_all_rk;my_inO).
	assert(HT1 : equivlist (P1 :: P2 :: P3 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil)) by (clear_all_rk;my_inO).
	assert(HT2 : equivlist (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: P4 :: P5 :: P8 :: P9 :: P10 :: nil) ((P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) ++ (P4 :: P5 :: P8 :: P9 :: P10 :: nil))) by (clear_all_rk;my_inO).
	try rewrite HT1 in HP1P2P3P4P5P8P9P10mtmp;try rewrite HT2 in HP1P2P3P4P5P8P9P10mtmp.
	assert(HT := rule_3 (P1 :: P2 :: P3 :: P8 :: P9 :: P10 :: nil) (P4 :: P5 :: P8 :: P9 :: P10 :: nil) (P8 :: P9 :: P10 :: nil) 3 3 4 HP1P2P3P8P9P10Mtmp HP4P5P8P9P10Mtmp HP1P2P3P4P5P8P9P10mtmp Hincl); apply HT.
}

assert(rk(P8 :: P9 :: P10 ::  nil) <= 3) by (clear_ineg_rk;try omega;try apply rk_upper_dim;try solve[apply matroid1_b_useful;simpl;intuition]).
assert(rk(P8 :: P9 :: P10 ::  nil) >= 1) by (clear_ineg_rk;try omega;try solve[apply matroid1_b_useful2;simpl;intuition]).
omega.
Qed.

author: ProjectiveGeometry

repo: ProjectiveGeometry


text:
Require Export RecTypes.SpecTypes.
Require Export RecTypes.InstTy.
Require Export RecTypes.Contraction.
Require Export StlcFix.Inst.
Require Export Coq.Relations.Relation_Operators.
Require Export Common.Relations.

(** ** Evaluation *)

Fixpoint Value (t: Tm) : Prop :=
  match t with
    | abs τ t      => True
    | unit         => True
    | true         => True
    | false        => True
    | pair t₁ t₂   => Value t₁ ∧ Value t₂
    | inl t        => Value t
    | inr t        => Value t
    | var _ | app _ _ | ite _ _ _
    | proj₁ _ | proj₂ _
    | caseof _ _ _
    | seq _ _
    | fixt _ _ _   => False
  end.

Fixpoint ECtx (C: PCtx) : Prop :=
  match C with
    | phole            => True
    | papp₁ C t        => ECtx C
    | papp₂ t C        => Value t ∧ ECtx C
    | pite₁ C t₂ t₃    => ECtx C
    | ppair₁ C t       => ECtx C
    | ppair₂ t C       => Value t ∧ ECtx C
    | pproj₁ C         => ECtx C
    | pproj₂ C         => ECtx C
    | pinl C           => ECtx C
    | pinr C           => ECtx C
    | pcaseof₁ C t₂ t₃ => ECtx C
    | pseq₁ C t        => ECtx C
    | pfixt τ₁ τ₂ C    => ECtx C
    | pabs _ _
    | pite₂ _ _ _ | pite₃ _ _ _
    | pcaseof₂ _ _ _ | pcaseof₃ _ _ _
    | pseq₂ _ _ => False
  end.

Reserved Notation "t₁ -->₀ t₂" (at level 80).
Inductive eval₀ : Tm → Tm → Prop :=
  | eval_beta {τ₁ t₁ t₂} :
      Value t₂ →
      app (abs τ₁ t₁) t₂ -->₀ t₁[beta1 t₂]
  | eval_ite_true {t₁ t₂} :
      ite true t₁ t₂ -->₀ t₁
  | eval_ite_false {t₁ t₂} :
      ite false t₁ t₂ -->₀ t₂
  | eval_proj₁ {t₁ t₂} :
      Value t₁ → Value t₂ →
      proj₁ (pair t₁ t₂) -->₀ t₁
  | eval_proj₂ {t₁ t₂} :
      Value t₁ → Value t₂ →
      proj₂ (pair t₁ t₂) -->₀ t₂
  | eval_case_inl {t t₁ t₂} :
      Value t →
      caseof (inl t) t₁ t₂ -->₀ t₁[beta1 t]
  | eval_case_inr {t t₁ t₂} :
      Value t →
      caseof (inr t) t₁ t₂ -->₀ t₂[beta1 t]
  | eval_seq_next {t₁ t₂} :
      Value t₁ →
      seq t₁ t₂ -->₀ t₂
  | eval_fix {τ₁ τ₂ t} :
      fixt τ₁ τ₂ (abs (τ₁ ⇒ τ₂) t) -->₀
      t[beta1 (abs τ₁ (app (fixt τ₁ τ₂ (abs (τ₁ ⇒ τ₂) t[wkm↑])) (var 0)))]
where "t₁ -->₀ t₂" := (eval₀ t₁ t₂).

Reserved Notation "t₁ --> t₂" (at level 80).
Inductive eval : Tm → Tm → Prop :=
| eval_ctx₀ C {t t'} :
    t -->₀ t' → ECtx C → pctx_app t C --> pctx_app t' C
where "t₁ --> t₂" := (eval t₁ t₂).

Notation "t -->i t'" := (eval t t') (at level 80).

#[export]
Hint Constructors eval : eval.
#[export]
Hint Constructors eval₀ : eval.
#[export]
Hint Constructors clos_refl_trans_1n : eval.
#[export]
Hint Constructors clos_trans_1n : eval.

Definition normal (t : Tm) := forall t', not (t --> t').

(* Alternative induction principle without program contexts. *)
Lemma eval_ind' (P: Tm → Tm → Prop) :
  (∀ (τ₁ : Ty) (t₁ t₂ : Tm), Value t₂ → P (app (abs τ₁ t₁) t₂) t₁[beta1 t₂]) →
  (∀ t₁ t₂ : Tm, P (ite true t₁ t₂) t₁) →
  (∀ t₁ t₂ : Tm, P (ite false t₁ t₂) t₂) →
  (∀ t₁ t₂ : Tm, Value t₁ → Value t₂ → P (proj₁ (pair t₁ t₂)) t₁) →
  (∀ t₁ t₂ : Tm, Value t₁ → Value t₂ → P (proj₂ (pair t₁ t₂)) t₂) →
  (∀ t t₁ t₂ : Tm, Value t → P (caseof (inl t) t₁ t₂) t₁[beta1 t]) →
  (∀ t t₁ t₂ : Tm, Value t → P (caseof (inr t) t₁ t₂) t₂[beta1 t]) →
  (∀ t₁ t₂ : Tm, Value t₁ → P (seq t₁ t₂) t₂) →
  (∀ (τ₁ τ₂ : Ty) (t : Tm),
     P (fixt τ₁ τ₂ (abs (τ₁ ⇒ τ₂) t))
       t[beta1 (abs τ₁ (app (fixt τ₁ τ₂ (abs (τ₁ ⇒ τ₂) t[wkm↑])) (var 0)))]) →
  (∀ t₁ t₁' t₂ : Tm, t₁ --> t₁' → P t₁ t₁' → P (app t₁ t₂) (app t₁' t₂)) →
  (∀ t₁ t₂ t₂' : Tm, Value t₁ → t₂ --> t₂' → P t₂ t₂' → P (app t₁ t₂) (app t₁ t₂')) →
  (∀ t₁ t₁' t₂ t₃ : Tm, t₁ --> t₁' → P t₁ t₁' → P (ite t₁ t₂ t₃) (ite t₁' t₂ t₃)) →
  (∀ t₁ t₁' t₂ : Tm, t₁ --> t₁' → P t₁ t₁' → P (pair t₁ t₂) (pair t₁' t₂)) →
  (∀ t₁ t₂ t₂' : Tm, Value t₁ → t₂ --> t₂' → P t₂ t₂' → P (pair t₁ t₂) (pair t₁ t₂')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (proj₁ t) (proj₁ t')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (proj₂ t) (proj₂ t')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (inl t) (inl t')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (inr t) (inr t')) →
  (∀ t₁ t₁' t₂ t₃ : Tm, t₁ --> t₁' → P t₁ t₁' → P (caseof t₁ t₂ t₃) (caseof t₁' t₂ t₃)) →
  (∀ t₁ t₁' t₂ : Tm, t₁ --> t₁' → P t₁ t₁' → P (seq t₁ t₂) (seq t₁' t₂)) →
  (∀ (τ₁ τ₂ : Ty) (t₁ t₁' : Tm), t₁ --> t₁' → P t₁ t₁' → P (fixt τ₁ τ₂ t₁) (fixt τ₁ τ₂ t₁')) →
  ∀ t t0 : Tm, t --> t0 → P t t0.
Proof.
  do 21 intro; induction 1 as [C ? ? r' ec].
  revert ec t t' r'.
  induction C; cbn in *; intuition.
  induction r'; cbn in *; intuition.
Qed.

(* The in-between induction principle *)
Lemma eval_ind'' (P: Tm → Tm → Prop) :
  (∀ t t' : Tm, t -->₀ t' → P t t') →
  (∀ t₁ t₁' t₂ : Tm, t₁ --> t₁' → P t₁ t₁' → P (app t₁ t₂) (app t₁' t₂)) →
  (∀ t₁ t₂ t₂' : Tm, Value t₁ → t₂ --> t₂' → P t₂ t₂' → P (app t₁ t₂) (app t₁ t₂')) →
  (∀ t₁ t₁' t₂ t₃ : Tm, t₁ --> t₁' → P t₁ t₁' → P (ite t₁ t₂ t₃) (ite t₁' t₂ t₃)) →
  (∀ t₁ t₁' t₂ : Tm, t₁ --> t₁' → P t₁ t₁' → P (pair t₁ t₂) (pair t₁' t₂)) →
  (∀ t₁ t₂ t₂' : Tm, Value t₁ → t₂ --> t₂' → P t₂ t₂' → P (pair t₁ t₂) (pair t₁ t₂')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (proj₁ t) (proj₁ t')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (proj₂ t) (proj₂ t')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (inl t) (inl t')) →
  (∀ t t' : Tm, t --> t' → P t t' → P (inr t) (inr t')) →
  (∀ t₁ t₁' t₂ t₃ : Tm, t₁ --> t₁' → P t₁ t₁' → P (caseof t₁ t₂ t₃) (caseof t₁' t₂ t₃)) →
  (∀ t₁ t₁' t₂ : Tm, t₁ --> t₁' → P t₁ t₁' → P (seq t₁ t₂) (seq t₁' t₂)) →
  (∀ (τ₁ τ₂ : Ty) (t₁ t₁' : Tm), t₁ --> t₁' → P t₁ t₁' → P (fixt τ₁ τ₂ t₁) (fixt τ₁ τ₂ t₁')) →
  ∀ t t0 : Tm, t --> t0 → P t t0.
Proof.
  do 13 intro; induction 1.
  induction C; cbn in *; intuition.
Qed.

Definition evaln := stepRel eval.

#[export]
Hint Constructors stepRel : eval.

Notation "t₁ -->* t₂" := (clos_refl_trans_1n Tm eval t₁ t₂) (at level 80).
Notation "⟪ 'F|' t₁ -->* t₂ ⟫" := (clos_refl_trans_1n Tm eval t₁ t₂) (at level 80).
Notation "t₁ -->+ t₂" := (clos_trans_1n Tm eval t₁ t₂) (at level 80).

(* TODO: get rid of this *)
Definition evalStar := clos_refl_trans_1n Tm eval.

Definition Terminating (t: Tm) : Prop :=
  ∃ v, Value v ∧ t -->* v.

Notation "t ⇓" := (Terminating t) (at level 8, format "t ⇓").
Notation "t ⇑" := (not (Terminating t)) (at level 8, format "t ⇑").

(* Terminates in maximum n steps *)
Definition TerminatingN (t: Tm) (n : nat) : Prop :=
  ∃ v m, Value v ∧ m ≤ n ∧ evaln t v m.
Notation "t ⇓_ n" := (TerminatingN t n) (at level 8, format "t ⇓_ n").

Section DerivedRules.

  Lemma eval_eval₀ {t t'} : t -->₀ t' -> t --> t'.
  Proof. intro r; now apply (eval_ctx₀ phole r). Qed.

  Lemma eval_beta'' {t₁ t₂ t' τ} :
    Value t₂ → t' = t₁[beta1 t₂] →
    app (abs τ t₁) t₂ -->₀ t'.
  Proof. intros; subst; auto using eval₀. Qed.

  Lemma eval_beta' {t₁ t₂ t' τ} :
    Value t₂ → t' = t₁[beta1 t₂] →
    app (abs τ t₁) t₂ --> t'.
  Proof. intros; apply eval_eval₀; subst; auto using eval₀. Qed.

  Lemma eval₀_case_inl' {t t₁ t₂ t'} :
    Value t → t' = t₁[beta1 t] →
    caseof (inl t) t₁ t₂ -->₀ t'.
  Proof. intros; subst; auto using eval₀. Qed.

  Lemma eval₀_case_inr' {t t₁ t₂ t'} :
    Value t → t' = t₂[beta1 t] →
    caseof (inr t) t₁ t₂ -->₀ t'.
  Proof. intros; subst; auto using eval₀. Qed.

  Lemma eval_case_inl' {t t₁ t₂ t'} :
    Value t → t' = t₁[beta1 t] →
    caseof (inl t) t₁ t₂ --> t'.
  Proof. intros; apply eval_eval₀; subst; auto using eval₀. Qed.

  Lemma eval_case_inr' {t t₁ t₂ t'} :
    Value t → t' = t₂[beta1 t] →
    caseof (inr t) t₁ t₂ --> t'.
  Proof. intros; apply eval_eval₀; subst; auto using eval₀. Qed.

End DerivedRules.

author: dominiquedevriese

repo: fixismu-coq


text:
(** * Equivalence *)

From Coq Require Import
  Classes.RelationClasses.
From DEZ.Is Require Export
  Reflexive Symmetric Transitive Preorder PartialEquivalence.

(** ** Equivalence Relation *)

Fail Fail Class IsEquiv (A : Type) (X : A -> A -> Prop) : Prop := {
  equiv_is_refl :> IsRefl X;
  equiv_is_sym :> IsSym X;
  equiv_is_trans :> IsTrans X;
}.

Arguments Equivalence {_} _.
Arguments Equivalence_Reflexive {_ _ _} _.
Arguments Equivalence_Symmetric {_ _ _} _ _ _.
Arguments Equivalence_Transitive {_ _ _} _ _ _ _ _.

Notation IsEquiv := Equivalence.
Notation equiv_is_refl := Equivalence_Reflexive.
Notation equiv_is_sym := Equivalence_Symmetric.
Notation equiv_is_trans := Equivalence_Transitive.

Section Context.

Context (A : Type) (X : A -> A -> Prop).

(** An equivalence relation is a preorder. *)

#[local] Instance equiv_is_preord
  `{!IsEquiv X} : IsPreord X.
Proof. typeclasses eauto. Qed.

(** An equivalence relation is a partial equivalence relation. *)

#[local] Instance equiv_is_part_equiv
  `{!IsEquiv X} : IsPartEquiv X.
Proof. typeclasses eauto. Qed.

End Context.

author: Tuplanolla

repo: dez

save_path: github-repos/coq/Tuplanolla-dez


text:
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Structures.Equalities.
Require Import Classes.EquivDec.
Require Import Program.Utils.
Require Import CakeSem.Utils.

Definition alist (X Y : Type) := list (X * Y).

Fixpoint range {K V : Type} (l : alist K V) : list V :=
  match l with
  | [] => []
  | (k,v)::l' => v::(range l')
  end.

(* Comes from somewhere else in Lem semantics *)
Inductive ident (X:Type) (Y:Type) : Type :=
  | Short : Y -> ident X Y
  | Long : X -> ident X Y -> ident X Y.

Arguments Short {X} {Y}.
Arguments Long {X} {Y}.

Fixpoint mk_id {M N: Type} (l : list M) (n : N) : ident M N :=
  match l with
  | [] => Short n
  | h :: t => Long h (mk_id t n)
  end.

Fixpoint id_to_n {M N : Type} (id : ident M N) : N :=
  match id with
  | Short n    => n
  | Long x id' => id_to_n id'
  end.

Fixpoint id_to_mods {M N : Type} (id : ident M N) : list M :=
  match id with
  | Short _ => []
  | Long m id' => m :: id_to_mods id'
  end.

Definition namespace (M N V : Type) := alist (ident M N) V.

Definition nsEmpty {M N V : Type} :=
  @nil ((ident M N) * V).

Fixpoint lookup {X Y : Type} (f : X -> X -> bool) (x : X) (l : alist X Y) : option Y :=
  match l with
  | [] => None
  | (x',y) :: l' => if f x x' then Some y else lookup f x l'
  end.

(* Namespace functions using a sumbool type for equality tests *)
Fixpoint lookup_dec {X Y : Type} (f : forall (x1 x2 : X), {x1 = x2} + {x1 <> x2}) (x : X) (l : alist X Y) : option Y :=
  match l with
  | [] => None
  | (x',y) :: l' => if f x x' then Some y else lookup_dec f x l'
  end.

Fixpoint get_modded_namespace_dec {M N V : Type} (f : forall (x1 x2 : M), {x1 = x2} + {x1 <> x2})
         (m : M) (ns : namespace M N V) : namespace M N V :=
  match ns with
  | [] => []
  | (i,v) :: ns' => match i with
                    | Short _ => get_modded_namespace_dec f m ns'
                    | Long m' i' => if f m m'
                                   then (i',v) :: (get_modded_namespace_dec f m ns')
                                   else get_modded_namespace_dec f m ns'
                  end
  end.

Definition nsLookup {M N V : Type} (f : ident M N -> ident M N -> bool)
           (id : ident M N) (ns : namespace M N V) : option V := lookup f id ns.

Definition nsLookup_dec {M N V : Type} (f : forall (x1 x2 : ident M N), {x1 = x2} + {x1 <> x2})
           (id : ident M N) (ns : namespace M N V) : option V := lookup_dec f id ns.

Fixpoint nsLookupMod_dec {M N V : Type} (f_dec : forall m1 m2 : M, {m1 = m2} + {m1 <> m2})
         (ns : namespace M N V) (xs : list M): option (namespace M N V) :=
  match xs, ns with
  | _, [] => None
  | [], ns => Some ns
  | m :: ms, ns => nsLookupMod_dec f_dec
                             (filter (fun '(i1,i2) => match i1 with
                                                   | Short n    => false
                                                   | Long  m' n => if f_dec m m' then true else false
                                                   end)
                                     ns)
                             ms
  end.

Definition nsAppend {M N V : Type} (ns1 : namespace M N V) (ns2 : namespace M N V) : namespace M N V :=
  ns1 ++ ns2.

Definition nsLift {M N V : Type} (m : M) (ns : namespace M N V) : namespace M N V :=
  map (fun '(i1,i2) => (Long m i1, i2)) ns.

Definition alist_to_ns {M N V : Type} (l : alist N V) : namespace M N V :=
  map (fun '(i1,i2) => (Short i1, i2)) l.

Definition nsBind {M N V : Type} (n : N) (v : V) (ns : namespace M N V) : namespace M N V :=
  (Short n, v) :: ns.

Definition nsBindList {M N V : Type} (l : alist N V) (ns : namespace M N V) : namespace M N V :=
  nsAppend (alist_to_ns l) ns.

Definition nsOptBind {M N V : Type} (n : option N) (v : V) (ns : namespace M N V) : namespace M N V :=
  match n with
  | None => ns
  | Some n' => nsBind n' v ns
  end.

Definition nsSing {M N V : Type} (n : N) (v : V) : namespace M N V :=
  [(Short n, v)].

Definition nsSub {M N V1 V2 : Type}
           (dec : forall (x y : ident M N), {x=y} + {x<>y})
           (rel : ident M N -> V1 -> V2 -> Prop)
           (ns1 : namespace M N V1)
           (ns2 : namespace M N V2) : Prop :=
     (forall (id : ident M N) (v1 : V1), nsLookup_dec dec id ns1 = Some v1 ->
       exists (v2 : V2), nsLookup_dec dec id ns2 = Some v2 /\ rel id v1 v2)
  /\ (forall (id : ident M N), nsLookup_dec dec id ns1 = None -> nsLookup_dec dec id ns2 = None).

Definition nsAll {M N V : Type} (dec : forall (x y : ident M N), {x=y} + {x<>y})
           (rel : ident M N -> V -> Prop)
           (ns : namespace M N V) : Prop :=
  (forall (id : ident M N) (v : V),
     nsLookup_dec dec id ns = Some v -> rel id v).

(* Definition eAll2 {M N V1 V2 : Type} (rel : ident M N -> V1 -> V2 -> Prop) *)
(*   (ns1 : namespace M N V1) (ns2 : namespace M N V2) : Prop := *)
(*   nsSub rel ns1 ns2 /\ nsSub (fun x y z => rel x z y) ns2 ns1. *)

Definition nsAll2 {M N V1 V2 : Type} (dec : forall (x y : ident M N), {x=y} + {x<>y})
           (rel : ident M N -> V1 -> V2 -> Prop)
           (ns1 : namespace M N V1)
           (ns2 : namespace M N V2) : Prop :=
  nsSub dec rel ns1 ns2 /\
  nsSub dec (fun x y z => rel x z y) ns2 ns1.

Definition extractIds {M N V : Type} (ns : namespace M N V) : list (ident M N) :=
  map fst ns.

Fixpoint extractMods {M N V : Type} (ns : namespace M N V) : list (list M) :=
  let get_ids := fix gids id :=
                   match id with
                   | Short _ => []
                   | Long m id' => m :: gids id'
                   end
  in
  match ns with
  | [] => []
  | (id,_)::ns' => get_ids id :: extractMods ns'
  end.

Definition nsMap {M N V W : Type} (f : V -> W)
         (ns : namespace M N V) : namespace M N W :=
  map (fun '(i1,i2) => (i1, f i2)) ns.

(* Namespace Theorems *)
Section NamespaceDec.
  Variable M : Type.
  Variable N : Type.
  Variable V : Type.
  Variable m_dec : forall (m0 m1 : M), {m0 = m1} + {m0 <> m1}.
  Variable n_dec : forall (n0 n1 : N), {n0 = n1} + {n0 <> n1}.
  Variable v_dec : forall (v0 v1 : V), {v0 = v1} + {v0 <> v1}.

  Theorem ident_eq_dec : forall (i0 i1 : ident M N),
      {i0 = i1} + {i0 <> i1}.
  Proof. decide equality.  Defined.

  Theorem namespace_eq_dec : forall (n0 n1 : namespace M N V), {n0 = n1} + {n0 <> n1}.
  Proof. decide equality. decide equality. apply ident_eq_dec. Defined.
End NamespaceDec.
#[export] Hint Resolve namespace_eq_dec : DecidableEquality.
#[export] Hint Resolve ident_eq_dec : DecidableEquality.

Section LookupTheory.
  Variable N : Type.
  Variable V : Type.
  Variable n_dec : forall (n0 n1 : N), {n0 = n1} + {n0 <> n1}.

  Lemma lookup_cover : forall (n : N) (ns ns' : alist N V) (v : V),
      lookup_dec n_dec n ns  = Some v ->
      lookup_dec n_dec n (ns ++ ns') = lookup_dec n_dec n ns.
  Proof.
    intros n ns ns' v.
    generalize dependent ns'.
    induction ns; intros ns' H.
    - inversion H.
    - destruct a. simpl. simpl in H. destruct n_dec.
      + reflexivity.
      + apply IHns. assumption.
  Qed.

  Lemma lookup_drop : forall (id : N) (ns ns' : alist N V),
      lookup_dec n_dec id ns = None ->
      lookup_dec n_dec id (ns ++ ns') = lookup_dec n_dec id ns'.
  Proof.
    intros id ns.
    induction ns; intros ns' H.
    - reflexivity.
    - destruct a; simpl in *. destruct n_dec.
      + inversion H.
      + apply IHns. assumption.
  Qed.

  Lemma lookup_same : forall (n : N) (ns : alist N V),
      lookup_dec n_dec n (ns ++ ns) = lookup_dec n_dec n ns.
  Proof.
    intros n ns.
    destruct (lookup_dec n_dec n ns) eqn:H; rewrite <- H.
    - apply lookup_cover with v; assumption.
    - apply lookup_drop; assumption.
  Qed.
End LookupTheory.

Section NamespaceTheory.
  Variable M : Type.
  Variable N : Type.
  Variable V : Type.
  Variable m_dec : forall (m0 m1 : M), {m0 = m1} + {m0 <> m1}.
  Variable n_dec : forall (n0 n1 : N), {n0 = n1} + {n0 <> n1}.
  Variable v_dec : forall (v0 v1 : V), {v0 = v1} + {v0 <> v1}.

  Definition id_dec := ident_eq_dec M N m_dec n_dec.

  Lemma get_modded_namespace_append : forall (ns ns' : namespace M N V) (x : M),
      get_modded_namespace_dec m_dec x (ns ++ ns') = (get_modded_namespace_dec m_dec x ns) ++ (get_modded_namespace_dec m_dec x ns').
  Proof.
    induction ns; intros ns' x.
    - reflexivity.
    - destruct a. destruct i.
      + apply IHns.
      + simpl. destruct (m_dec x m).
        * simpl. rewrite IHns. reflexivity.
        * simpl. apply IHns.
  Qed.

  Lemma nsLookup_cover : forall (id : ident M N) (ns ns' : namespace M N V) (v : V),
      nsLookup_dec id_dec id ns = Some v ->
      nsLookup_dec id_dec id (ns ++ ns') = nsLookup_dec id_dec id ns.
  Proof.
    intros. unfold nsLookup_dec in *. apply lookup_cover with v. assumption.
  Qed.

  Lemma nsLookup_drop : forall (id : ident M N) (ns ns' : namespace M N V),
      nsLookup_dec id_dec id ns = None ->
      nsLookup_dec id_dec id (ns ++ ns') = nsLookup_dec id_dec id ns'.
  Proof.
    intros id ns ns' H.
    unfold nsLookup_dec in *. apply lookup_drop. assumption.
  Qed.

  Lemma nsLookup_same : forall (id : ident M N) (ns : namespace M N V),
      nsLookup_dec id_dec id (ns ++ ns) = nsLookup_dec id_dec id ns.
  Proof.
    intros id ns.
    unfold nsLookup_dec in *. apply lookup_same.
  Qed.

End NamespaceTheory.

author: ku-sldg

repo: cakeml-coq

save_path: github-repos/coq/ku-sldg-cakeml-coq