-definition same_values_simpl ≝
- λl1,l2:list bar.∀H1,H2,H3,H4,input,Hi1,Hi2.
- value_simpl l1 H1 H2 input Hi1 = value_simpl l2 H3 H4 input Hi2.
-
-lemma value_head :
- ∀x,y,l,H1,H2,i,H3.
- Qpos i ≤ \fst x → value_simpl (y::x::l) H1 H2 i H3 = \snd y.
-intros; cases (cases_value_simpl ? H1 H2 i H3);
-cases j in H4 H5 H6 H7 H8 (j); simplify; intros;
-[1: symmetry; assumption;
-|2: cases (?:False); cases j in H4 H5 H6 H7 H8; intros;
- [1: lapply (q_le_lt_trans ??? H H5) as K;cases (q_lt_corefl ? K);
- |2: lapply (H7 1); [2: do 2 apply le_S_S; apply le_O_n;]
- simplify in Hletin;
- lapply (q_le_lt_trans ??? H Hletin) as K;cases (q_lt_corefl ? K);]]
-qed.
-
-lemma same_values_simpl_to_same_values:
- ∀b1,b2,Hs1,Hs2,Hb1,Hb2,He1,He2,input.
- same_values_simpl b1 b2 →
- value (mk_q_f b1 Hs1 Hb1 He1) input =
- value (mk_q_f b2 Hs2 Hb2 He2) input.
-intros;
-lapply (len_bases_gt_O (mk_q_f b1 Hs1 Hb1 He1));
-lapply (len_bases_gt_O (mk_q_f b2 Hs2 Hb2 He2));
-lapply (H ???? input) as K; try assumption;
-[2: rewrite > Hb1; apply q_pos_OQ;
-|3: rewrite > Hb2; apply q_pos_OQ;
-|1: apply K;]
-qed.
-
-include "russell_support.ma".
-
-lemma value_tail :
- ∀x,y,l,H1,H2,i,H3.
- \fst x < Qpos i →
- value_simpl (y::x::l) H1 H2 i H3 =
- value_simpl (x::l) ?? i ?.
-[1: apply hide; apply (sorted_tail q2_lt); [apply y| assumption]
-|2: apply hide; simplify; apply le_S_S; apply le_O_n;
-|3: apply hide; assumption;]
-intros;cases (cases_value_simpl ? H1 H2 i H3);
-generalize in ⊢ (? ? ? (? ? % ? ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? % ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? ? ? %)); intro;
-cases (cases_value_simpl (x::l) H9 H10 i H11);
-cut (j = S j1) as E; [ destruct E; destruct H12; reflexivity;]
-clear H12 H4; cases j in H8 H5 H6 H7;
-[1: intros;cases (?:False); lapply (H7 1 (le_n ?)); [2: simplify; do 2 apply le_S_S; apply le_O_n]
- simplify in Hletin; apply (q_lt_corefl (\fst x));
- apply (q_lt_le_trans ??? H Hletin);
-|2: simplify; intros; clear q q1 j H11 H10 H1 H2; simplify in H3 H14; apply eq_f;
- cases (cmp_nat n j1); [cases (cmp_nat j1 n);[apply le_to_le_to_eq; assumption]]
- [1: clear H1; cases (?:False);
- lapply (H7 (S j1)); [2: cases j1 in H2; intros[cases (not_le_Sn_O ? H1)] apply le_S_S; assumption]
- [2: apply le_S_S; assumption;] simplify in Hletin;
- apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H13));
- |2: cases (?:False);
- lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption]
- apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]]
-qed.
-
-lemma value_unit:
- ∀x,i,h1,h2,h3.value_simpl [x] h1 h2 i h3 = \snd x.
-intros; cases (cases_value_simpl [x] h1 h2 i h3); cases j in H H2; simplify;
-intros; [2: cases (?:False); apply (not_le_Sn_O n); apply le_S_S_to_le; apply H2]
-symmetry; assumption;
-qed.
-
-lemma same_value_tail:
- ∀b,b1,h1,h3,xs,r1,input,H12,H13,Hi1,H14,H15,Hi2.
- same_values_simpl (〈b1,h1〉::xs) (〈b1,h3〉::r1) →
- value_simpl (b::〈b1,h1〉::xs) H12 H13 input Hi1
- =value_simpl (b::〈b1,h3〉::r1) H14 H15 input Hi2.
-intros; cases (q_cmp (Qpos input) b1);
-[1: rewrite > (value_head 〈b1,h1〉 b xs); [2:assumption]
- rewrite > (value_head 〈b1,h3〉 b r1); [2:assumption] reflexivity;
-|2: rewrite > (value_tail 〈b1,h1〉 b xs);[2: assumption]
- rewrite > (value_tail 〈b1,h3〉 b r1);[2: assumption] apply H;]
-qed.