|3: apply H; apply le_S_S_to_le; assumption;]
qed.
-definition copy ≝
- λl:list bar.make_list ? (λn.〈nth_base l (\len l - S n),〈OQ,OQ〉〉) (\len l).
+alias symbol "lt" = "bar lt".
+lemma inversion_sorted:
+ ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
+intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
+[1,2:destruct H2| destruct H5; assumption]
+qed.
+
+lemma inversion_sorted2:
+ ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
+intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption;
+qed.
+
+let rec copy (l : list bar) on l : list bar ≝
+ match l with
+ [ nil ⇒ []
+ | cons x tl ⇒ 〈\fst x, 〈OQ,OQ〉〉 :: copy tl].
lemma sorted_copy:
∀l:list bar.sorted q2_lt l → sorted q2_lt (copy l).
-intros 2; unfold copy; generalize in match (le_n (\len l));
-elim (\len l) in ⊢ (?%?→? ? (? ? ? %));
-simplify; [apply (sorted_nil q2_lt);] cases n in H1 H2;
-simplify; intros; [apply (sorted_one q2_lt);]
-apply (sorted_cons q2_lt);
-[2: apply H1; apply lt_to_le; apply H2;
-|1: elim l in H2 H; simplify; [simplify in H2; cases (not_le_Sn_O ? H2)]
- simplify in H3; unfold nth_base;
- unfold canonical_q_lt; unfold q2_trel; unfold q2_lt; simplify;
- change with (q2_lt (\nth (a::l1) ▭ (\len l1-S n1)) (\nth (a::l1) ▭ (\len l1-n1)));
- cut (∃w.w = \len l1 - S n1); [2: exists[apply (\len l1 - S n1)] reflexivity]
- cases Hcut; rewrite < H4; rewrite < (?:S w = \len l1 - n1);
- [1: apply (sorted_near q2_lt (a::l1) H2); rewrite > H4;
- simplify; apply le_S_S; elim (\len l1) in H3; simplify;
- [ cases (not_le_Sn_O ? (le_S_S_to_le ?? H3));
- | lapply le_S_S_to_le to H5 as H6;
- lapply le_S_S_to_le to H6 as H7; clear H5 H6;
- cases H7 in H3; intros; [rewrite < minus_n_n; apply le_S_S; apply le_O_n]
- simplify in H5; apply le_S_S; apply (trans_le ???? (H5 ?));
- [2: apply le_S_S; apply le_S_S; assumption;
- |1: apply (lt_minus_S_n_to_le_minus_n n1 (S m) (S (minus m n1)) ?).
- apply (not_le_to_lt (S (minus m n1)) (minus (S m) (S n1)) ?).
- apply (not_le_Sn_n (minus (S m) (S n1))).]]
- |2: rewrite > H4; lapply le_S_S_to_le to H3 as K;
- clear H4 Hcut H3 H H1 H2; generalize in match K; clear K;
- apply (nat_elim2 ???? n1 (\len l1)); simplify; intros;
- [1: rewrite < minus_n_O; cases n2 in H; [intro; cases (not_le_Sn_O ? H)]
- intros; cases n3; simplify; reflexivity;
- |2: cases (not_le_Sn_O ? H);
- |3: apply H; apply le_S_S_to_le; apply H1;]]]
+intro l; elim l; [apply (sorted_nil q2_lt)] simplify;
+cases l1 in H H1; simplify; intros; [apply (sorted_one q2_lt)]
+apply (sorted_cons q2_lt); [2: apply H; apply (sorted_tail q2_lt ?? H1);]
+apply (inversion_sorted2 ??? H1);
qed.
lemma len_copy: ∀l. \len (copy l) = \len l.
-intro; unfold copy; apply len_mk_list;
+intro; elim l; [reflexivity] simplify; apply eq_f; assumption;
qed.
lemma copy_same_bases: ∀l. same_bases l (copy l).
-intro; unfold copy; elim l using list_elim_with_len; [1: intro;reflexivity]
-simplify; rewrite < minus_n_n;
-simplify in ⊢ (? ? (? ? (? ? ? % ?) ?));
-apply same_bases_cons; [2: reflexivity]
-cases l1 in H; [intros 2; reflexivity]
-simplify in ⊢ (? ? (? ? (λ_:?.? ? ? (? ? %) ?) ?)→?);
-simplify in ⊢ (?→? ? (? ? (λ_:?.? ? ? (? ? (? % ?)) ?) ?));
-intro; rewrite > (mk_list_ext ?? (λn:nat.〈nth_base (b::l2) (\len l2-n),〈OQ,OQ〉〉));[assumption]
-intro; elim x; [simplify; rewrite < minus_n_O; reflexivity]
-simplify in ⊢ (? ? (? ? ? (? ? %) ?) ?);
-simplify in H2:(? ? %); rewrite > minus_lt; [reflexivity] apply le_S_S_to_le;
-assumption;
-qed.
-
-lemma rewrite_ext_nth_height : ∀n,m,f,f1,g,g1. (∀t.g t = g1 t) →
-nth_height (\mk_list (λn.〈f n,g n〉) m) n = nth_height (\mk_list (λn.〈f1 n,g1 n〉) m) n.
-intros; generalize in match n; clear n; elim m; [reflexivity] simplify;
-cases n1; [simplify;apply H;] simplify; apply (H1 n2);
+intros; elim l; [intro; reflexivity] intro; simplify; cases i; [reflexivity]
+simplify; apply (H n);
qed.
lemma copy_OQ : ∀l,n.nth_height (copy l) n = 〈OQ,OQ〉.
-intro; elim l; [cases n; [reflexivity] simplify; rewrite > nth_nil; reflexivity]
-cases n; simplify [reflexivity]
-change with (nth_height (\mk_list (λn:ℕ.〈nth_base (a::l1) (\len l1-n),〈OQ,OQ〉〉) (\len l1)) n1 = 〈OQ,OQ〉);
-rewrite > (rewrite_ext_nth_height ??? (λ_.OQ) ? (λ_.〈OQ,OQ〉)); [2: intros; reflexivity]
-generalize in match n1;
-elim (\len l1); simplify; unfold nth_height; [rewrite > nth_nil; reflexivity]
-cases n3; simplify; [reflexivity] apply (H1 n4);
+intro; elim l; [elim n;[reflexivity] simplify; assumption]
+simplify; cases n; [reflexivity] simplify; apply (H n1);
qed.
lemma prepend_sorted_with_same_head:
|2: cases (H3 H4);]
qed.
-alias symbol "lt" = "bar lt".
-lemma inversion_sorted:
- ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
-intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
-[1,2:destruct H2| destruct H5; assumption]
-qed.
-
-lemma inversion_sorted2:
- ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
-intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption;
-qed.
lemma sort_q2lt_same_base:
∀b,h1,h2,l. sorted q2_lt (〈b,h1〉::l) → sorted q2_lt (〈b,h2〉::l).
[apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
qed.
+lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a.
+intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭);
+[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;]
+ simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K;
+ simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K);
+|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;]
+ unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin;
+ simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);]
+qed.
+
+lemma value_unit : ∀x,i. value_simple [x] i = \snd x.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) [x] ▭);
+[1: cases i1 in H; intros; [reflexivity] simplify in H;
+ cases (not_le_Sn_O ? (le_S_S_to_le ?? H));
+|2: simplify in H; destruct H; reflexivity;]
+qed.
+
+lemma value_tail :
+ ∀a,b,l,i.\fst a < Qpos i → \fst b ≤ Qpos i → value_simple (a::b::l) i = value_simple (b::l) i.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) (a::b::l) ▭);
+[1: cases i1 in H3 H2 H4 H5; intros 1; simplify in ⊢ (? ? (? ? %) ?→?); unfold in ⊢ (? ? % ?→?); intros;
+ [1: cases (?:False); cases (q_cmp (Qpos i) (\fst a)) in H3; simplify; intros;[2: destruct H6]
+ apply (q_lt_corefl ? (q_lt_le_trans ??? H H3));
+ |2:
+
+normalize in ⊢ (? ? % ?→?); simplify;
+[1: rewrite > (value_head);
+
+lemma value_copy :
+ ∀l,i.rewrite > (value_u
+ value_simple (copy l) i = 〈OQ,OQ〉.
+intros; elim l;
+[1: reflexivity;
+|2: cases l1 in H; intros; simplify in ⊢ (? ? (? % ?) ?);
+ [1: rewrite > (value_unit); reflexivity;
+ |2: cases (q_cmp (\fst b) (Qpos i));
+
+ change with (\fst ▭ = \lamsimplify in ⊢ (? ? (? % ?) ?); unfold value_simple; unfold match_domain;
+ cases (cases_find bar (match_pred i) [〈\fst x,〈OQ,OQ〉〉] ▭);
+ [1: simplify in H1:(??%%);
+
+ unfold match_pred;
+ rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity;
+|2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?);
+ cases (q_cmp (Qpos i) (\fst b));
+ [2: rewrite > (value_tail ??? H2 H3 ? H4 H1); apply H;
+ |1: rewrite > (value_head ??? H2 H3 ? H4 H1); reflexivity]]
+qed.
+
\ No newline at end of file
projects / helm.git / blobdiff