-bishop_set.ma ordered_set.ma
-nat_ordered_set.ma bishop_set.ma nat/compare.ma
-models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
-models/q_rebase.ma Q/q/qtimes.ma models/q_function.ma
property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
-ordered_uniform.ma uniform.ma
-models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
-models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
-ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma
-models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/minus.ma
-uniform.ma supremum.ma
-sandwich.ma ordered_uniform.ma
-models/q_value_skip.ma
-models/q_shift.ma
+sequence.ma nat/nat.ma
+supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
+property_sigma.ma ordered_uniform.ma russell_support.ma
+bishop_set_rewrite.ma bishop_set.ma
models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma logic/cprop_connectives.ma
+sandwich.ma ordered_uniform.ma
+nat_ordered_set.ma bishop_set.ma nat/compare.ma
+ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma
+models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma russell_support.ma
-models/q_copy.ma models/q_bars.ma
-models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
-property_sigma.ma ordered_uniform.ma russell_support.ma
+models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/le_arith.ma nat/minus.ma
+bishop_set.ma ordered_set.ma
lebesgue.ma property_exhaustivity.ma sandwich.ma
+models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
-models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
-bishop_set_rewrite.ma bishop_set.ma
russell_support.ma logic/cprop_connectives.ma nat/nat.ma
-.unnamed.ma models/q_bars.ma
-supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
+models/q_copy.ma models/q_bars.ma
+models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
+models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
models/q_function.ma models/q_copy.ma russell_support.ma
-sequence.ma nat/nat.ma
+models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
+uniform.ma supremum.ma
+ordered_uniform.ma uniform.ma
+models/q_rebase.ma Q/q/qtimes.ma models/q_function.ma
Q/q/qplus.ma
Q/q/qtimes.ma
datatypes/constructors.ma
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.
+
definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i).
lemma same_bases_cons: ∀a,b,l1,l2.
|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
(same_values l2 (\snd p)).
inductive rebase_cases : list bar → list bar → (list bar) × (list bar) → Prop ≝
-| rb_fst_full : ∀b,h1,xs. (*〈b,h1〉 < \hd ▭ ys → *)
-(* \snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h1〉::r1)) →
- \snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h2〉::r2)) →*)
+| rb_fst_full : ∀b,h1,xs.
rebase_cases (〈b,h1〉::xs) [] 〈〈b,h1〉::xs,〈b,〈OQ,OQ〉〉::copy xs〉
-| rb_snd_full : ∀b,h1,ys. (*〈b,h1〉 < \hd ▭ xs →*)
- (* \snd(\last ▭ (〈b,h1〉::ys)) = \snd(\last ▭ (〈b,h1〉::r2)) →
- \snd(\last ▭ (〈b,h1〉::ys)) = \snd(\last ▭ (〈b,h2〉::r1)) →*)
+| rb_snd_full : ∀b,h1,ys.
rebase_cases [] (〈b,h1〉::ys) 〈〈b,〈OQ,OQ〉〉::copy ys,〈b,h1〉::ys〉
| rb_all_full : ∀b,h1,h2,h3,h4,xs,ys,r1,r2.
\snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h3〉::r1)) →
\snd(\last ▭ (〈b1,h1〉::xs)) = \snd(\last ▭ (〈b1,h1〉::r1)) →
\snd(\last ▭ (〈b2,h2〉::ys)) = \snd(\last ▭ (〈b1,h2〉::r2)) →
b1 < b2 →
- rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b1,h1〉::r1,〈b1,h2〉::r2〉
+ rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b1,h1〉::r1,〈b1,〈OQ,OQ〉〉::r2〉
| rb_all_full_r : ∀b1,b2,h1,h2,xs,ys,r1,r2.
\snd(\last ▭ (〈b1,h1〉::xs)) = \snd(\last ▭ (〈b2,h1〉::r1)) →
\snd(\last ▭ (〈b2,h2〉::ys)) = \snd(\last ▭ (〈b2,h2〉::r2)) →
b2 < b1 →
- rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b2,h1〉::r1,〈b2,h2〉::r2〉
+ rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b2,〈OQ,OQ〉〉::r1,〈b2,h2〉::r2〉
| rb_all_empty : rebase_cases [] [] 〈[],[]〉.
alias symbol "pi2" = "pair pi2".
| prove_rebase_spec_aux:
rebase_cases l1 l2 p →
(sorted q2_lt (\fst p)) →
- (sorted q2_lt (\snd p)) → True → True → (*
- ((l1 ≠ [] ∧ \snd (\last ▭ (\fst p)) = 〈OQ,OQ〉) ∨
- (l1 = [] ∧ ∀i.\snd (\nth (\fst p) ▭ i) = 〈OQ,OQ〉)) →
- ((l2 ≠ [] ∧ \snd (\last ▭ (\snd p)) = 〈OQ,OQ〉) ∨
- (l2 = [] ∧ ∀i.\snd (\nth (\snd p) ▭ i) = 〈OQ,OQ〉)) →*)
+ (sorted q2_lt (\snd p)) →
(same_bases (\fst p) (\snd p)) →
(same_values_simpl l1 (\fst p)) →
(same_values_simpl l2 (\snd p)) →
- (*\len (\fst p) ≤ \len l1 + \len l2 → *)
- (*\len (\fst p) = \len (\snd p) → *)
rebase_spec_aux_p l1 l2 p.
lemma aux_preserves_sorting:
(**************************************************************************)
include "models/q_function.ma".
-
+
+alias symbol "lt" = "Q less than".
+alias symbol "Q" = "Rationals".
+axiom q_unlimited: ∀x:ℚ.∃y:ratio.x<Qpos y.
+axiom q_halving: ∀x,y:ℚ.∃z:ℚ.x<z ∧ z<y.
+lemma same_values_unit_OQ:
+ ∀b1,b2,h1,l. b2 < b1 → sorted q2_lt (〈b1,h1〉::l) →
+ sorted q2_lt [〈b2,〈OQ,OQ〉〉] →
+ same_values_simpl (〈b1,h1〉::l) [〈b2,〈OQ,OQ〉〉] → h1 = 〈OQ,OQ〉.
+intros 4; cases l;
+[1: intros; cases (q_unlimited b1); cut (b2 < Qpos w); [2:apply (q_lt_trans ??? H H4);]
+ lapply (H3 H1 ? H2 ? w H4 Hcut) as K; simplify; [1,2: autobatch]
+ rewrite > (value_unit 〈b1,h1〉) in K;
+ rewrite > (value_unit 〈b2,〈OQ,OQ〉〉) in K; assumption;
+|2: intros; (* MANCA che le basi sono positive,
+ poi con halving prendi tra b1 e \fst p e hai h1=OQ,OQ*)
+
+
definition eject ≝
λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p].
coercion eject.
[7: clearbody aux; cases (aux b1 b2 (\len b1 + \len b2)) (res Hres);
exists; [split; constructor 1; [apply (\fst res)|5:apply (\snd res)]]
[1,4: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); assumption;
- |2,5: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); lapply (H5 O) as K;
- clear H1 H2 H3 H4 H5 H6 H7 Hres aux; unfold nth_base;
+ |2,5: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres aux;
+ lapply (H3 O) as K; clear H1 H2 H3 H4 H5; unfold nth_base;
cases H in K He1 He2 Hb1 Hb2; simplify; intros; assumption;
- |3,6: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2);
+ |3,6: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres aux;
cases H in He1 He2; simplify; intros;
[1,6,8,12: assumption;
|2,7: rewrite > len_copy; generalize in match (\len ?); intro X;
cases X; [1,3: reflexivity] simplify;
[apply (copy_OQ ys n);|apply (copy_OQ xs n);]
- |3,4,5: rewrite < H8; assumption;
- |9,10,11: rewrite < H9; assumption]]
- split; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); unfold same_values; intros;
+ |3,4: rewrite < H6; assumption;
+ |5: cases r1 in H6; simplify; intros; [reflexivity] rewrite < H6; assumption;
+ |9,11: rewrite < H7; assumption;
+ |10: cases r2 in H7; simplify; intros; [reflexivity] rewrite < H7; assumption]]
+ split; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres; unfold same_values; intros;
[1: assumption
|2,3: simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉);
apply same_values_simpl_to_same_values; assumption]
|3: cut (\fst b3 = \fst b) as E; [2: apply q_le_to_le_to_eq; assumption]
- clear H6 H5 H4 H3 He2 Hb2 Hs2 b2 He1 Hb1 Hs1 b1; cases (aux l2 l3 n1);
+ clear H6 H5 H4 H3 He2 Hb2 Hs2 b2 He1 Hb1 Hs1 b1; cases (aux l2 l3 n1) (rc Hrc);
clear aux; intro K; simplify in K; rewrite <plus_n_Sm in K;
lapply le_S_S_to_le to K as W; lapply lt_to_le to W as R;
- simplify in match (? ≪w,H3≫); intros; cases (H3 R); clear H3 R W K;
+ simplify in match (? ≪rc,Hrc≫); intros (Hsbl2 Hendbl2 Hsb3l3 Hendb3l3);
+ change in Hendbl2 with (\snd (\last ▭ (b::l2)) = 〈OQ,OQ〉);
+ change in Hendb3l3 with (\snd (\last ▭ (b3::l3)) = 〈OQ,OQ〉);
+ cases (Hrc R) (RC S1 S2 SB SV1 SV2); clear Hrc R W K;
[2,4: apply (sorted_tail q2_lt);[apply b|3:apply b3]assumption;
- |3: cases l2 in H5; simplify; intros; try reflexivity; assumption;
- |5: cases l3 in H7; simplify; intros; try reflexivity; assumption;]
+ |3: cases l2 in Hendbl2; simplify; intros; [reflexivity] assumption;
+ |5: cases l3 in Hendb3l3; simplify; intros; [reflexivity] assumption;]
constructor 1; simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉);
- [1: cases b in E H5 H7 H11 H14; cases b3; intros (E H5 H7 H11 H14); simplify in E;
- destruct E; constructor 3;
- [ cases H8 in H5 H7; intros; [1,6:reflexivity|3,4,5: assumption;]
- simplify; rewrite > H3; rewrite > len_copy; elim (\len ys); [reflexivity]
+ [1: cases b in E Hsbl2 Hendbl2; cases b3 in Hsb3l3 Hendb3l3; intros (Hsbl3 Hendbl2 E Hsb3l2 Hendb3l3);
+ simplify in E; destruct E; constructor 3;
+ [1: clear Hendbl2 Hsbl3 SV2 SB S2;
+ cases RC in S1 SV1 Hsb3l2 Hendb3l3; intros;
+ [1,6: reflexivity;
+ |3,4: assumption;
+ |5: simplify in H6:(??%) ⊢ %; rewrite > H3; cases r1 in H6; intros [2:reflexivity]
+ use same_values_unit_OQ;
+
+ |2: simplify in H3:(??%) ⊢ %; rewrite > H3; rewrite > len_copy; elim (\len ys); [reflexivity]
symmetry; apply (copy_OQ ys n2);
| cases H8 in H5 H7; simplify; intros; [2,6:reflexivity|3,4,5: assumption]
simplify; rewrite > H5; rewrite > len_copy; elim (\len xs); [reflexivity]
|4: apply I
|5: apply I
|6: intro; elim i; intros; simplify; solve [symmetry;assumption|apply H13]
- |7: unfold; intros; cases H8 in H13 H14 H15 Hi1 Hi2 H17 H18 H3 H16; intros;
- [1: simplify in match (\fst 〈?,?〉) in H16 H17 H20 H21 H22 H23 ⊢ %;
- cases (q_cmp (Qpos input) b1);
- [1: do 2 (rewrite > value_head; [id|assumption]); reflexivity;
- |2: do 2 (rewrite > value_tail;[id|assumption]); apply H16;]
- |2: simplify in match (\fst 〈?,?〉) in H16 H17 H20 H21 H22 H23 ⊢ %;
- cases (q_cmp (Qpos input) b1);
- [1: rewrite > value_head; [2:assumption]
- |2: rewrite > value_tail;[2:assumption]
- simplify in H15;
+ |7: unfold; intros; clear H9 H10 H11 H12 H13; simplify in Hi1 Hi2 H16 H18;
+ cases H8 in H14 H15 H17 H3 H16 H18 H5 H6;
+ simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉); intros;
+ [1: reflexivity;
+ |2: simplify in H3; rewrite > (value_unit b); rewrite > H3; symmetry;
+ cases b in H3 H12 Hi2; intros 2; simplify in H12; rewrite > H12;
+ intros; change in ⊢ (? ? (? % ? ? ? ?) ?) with (copy (〈q,〈OQ,OQ〉〉::〈b1,〈OQ,OQ〉〉::ys));
+ apply (value_copy (〈q,〈OQ,OQ〉〉::〈b1,〈OQ,OQ〉〉::ys));
+ |3: apply (same_value_tail b b1 h1 h3 xs r1 input); assumption;
+ |4: apply (same_value_tail b b1 h1 h1 xs r1 input); assumption;
+ |5: simplify in H9; STOP
+
+ |6: reflexivity;]
+
]
|8:
projects / helm.git / commitdiff
