|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_copy :
+ ∀l,h1,h2,i,h3.
+ value_simpl (copy l) h1 h2 i h3 = 〈OQ,OQ〉.
+intros; elim l in h1 h2 h3; [cases (not_le_Sn_O ? H1);]
+cases l1 in H H1 H2 H3;
+[1: intros; simplify in ⊢ (? ? (? % ? ? ? ?) ?);
+ 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