diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-07-12 14:58:06 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:30 +0200 |
commit | edb93401b3621e8e9731c0a50afdbcc441d7f495 (patch) | |
tree | e33666d69f732b6709f59450910a13f0473331aa /mppa_k1c | |
parent | 2e93b668df554edbfec0c23de7b14caf95a48b1d (diff) | |
download | compcert-kvx-edb93401b3621e8e9731c0a50afdbcc441d7f495.tar.gz compcert-kvx-edb93401b3621e8e9731c0a50afdbcc441d7f495.zip |
Machblock: some renaming and proof simplifications
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Machblockgen.v | 294 | ||||
-rw-r--r-- | mppa_k1c/Machblockgenproof.v | 71 |
2 files changed, 144 insertions, 221 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 0601f5b9..aa54e8a2 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -94,51 +94,21 @@ Proof. destruct i; discriminate. Qed. -Lemma get_code_nature_nil_contra c: get_code_nature c = IsEmpty -> c = nil. +Lemma get_code_nature_empty c: get_code_nature c = IsEmpty -> c = nil. Proof. intros H. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto. intro F. contradict F. Qed. -Lemma get_code_nature_basic_inst c a c0: - c = a :: c0 -> - get_code_nature c = IsBasicInst -> - to_basic_inst a <> None. -Proof. - intros H1 H2. destruct a; discriminate || contradict H2; subst; simpl; discriminate. -Qed. - -Lemma to_bblock_header_not_IsLabel c h c0: - get_code_nature c <> IsLabel -> - to_bblock_header c = (h, c0) -> - c = c0 /\ h=nil. -Proof. - intros H1 H2. destruct c. - - simpl in H2; inversion H2; auto. - - destruct i; unfold to_bblock_header in H2; inversion H2; auto. - simpl in H1; contradict H1; auto. -Qed. - -Lemma to_bblock_header_eq c h c0: +Lemma to_bblock_header_noLabel c: get_code_nature c <> IsLabel -> - to_bblock_header c = (h, c0) -> - c = c0. + to_bblock_header c = (nil, c). Proof. - intros H1 H2; exploit to_bblock_header_not_IsLabel; intuition eauto. + intros H. destruct c as [|i c]; auto. + destruct i; simpl; auto. + contradict H; simpl; auto. Qed. -(* -Lemma to_bblock_header_IsLabel c c0 b: - get_code_nature c = IsLabel -> - to_bblock_header c = (b, c0) -> - exists l, c = (Mlabel l)::c0. -Proof. - intros H1 H2. destruct c; try discriminate. - destruct i; try discriminate. - unfold to_bblock_header in H2; inversion H2; eauto. -Qed. -*) - Lemma to_bblock_header_wfe c: forall h c0, to_bblock_header c = (h, c0) -> @@ -166,15 +136,13 @@ Proof. simpl; omega. Qed. -Lemma to_bblock_body_eq c b c0: +Lemma to_bblock_body_noBasic c: get_code_nature c <> IsBasicInst -> - to_bblock_body c = (b, c0) -> - c = c0. + to_bblock_body c = (nil, c). Proof. - intros H1 H2. destruct c. - - simpl in H2. inversion H2. auto. - - destruct i; try ( simpl in *; destruct H1; auto; fail ). - all: simpl in *; inversion H2; subst; clear H2; auto. + intros H. destruct c as [|i c]; simpl; auto. + destruct i; simpl; auto. + all: contradict H; simpl; auto. Qed. Lemma to_bblock_body_wfe c b c0: @@ -190,7 +158,35 @@ Proof. + inversion H; subst; auto. Qed. -(* pas vraiment utile: à éliminer *) +(** Attempt to eliminate cons_to_bblock_body *) +(* +Lemma to_bblock_body_basic c: + get_code_nature c = IsBasicInst -> + exists i bi b c', + to_basic_inst i = Some bi + /\ c = i :: c' + /\ to_bblock_body c = (bi::b, snd (to_bblock_body c')). +Proof. + intros H. + destruct c as [|i c]; try (contradict H; simpl; discriminate). + destruct i eqn:I; try (contradict H; simpl; discriminate). + all: simpl; destruct (to_bblock_body c) as [p c''] eqn:TBBC; repeat (eapply ex_intro); (repeat split); + simpl; eauto; rewrite TBBC; simpl; eauto. +Qed. + +Lemma to_bblock_body_wf c b c0: + get_code_nature c = IsBasicInst -> + to_bblock_body c = (b, c0) -> + (length c > length c0)%nat. +Proof. + intros H1 H2; exploit to_bblock_body_basic; eauto. + intros X. destruct X as (i & bi & b' & c' & X1 & X2 & X3). + exploit to_bblock_body_wfe. eauto. subst. simpl. + rewrite X3 in H2. inversion H2; clear H2; subst. + simpl; omega. +Qed. +*) + Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop := Cons_to_bbloc_body i bi c' b': to_basic_inst i = Some bi @@ -216,20 +212,18 @@ Lemma to_bblock_body_wf c b c0: (length c > length c0)%nat. Proof. intros H1 H2; exploit to_bblock_body_IsBasicInst; eauto. - intros X; destruct X. - exploit to_bblock_body_wfe; eauto. + intros X. destruct X. + exploit to_bblock_body_wfe; eauto. subst. simpl. simpl; omega. Qed. -Lemma to_bblock_exit_eq c b c0: +Lemma to_bblock_exit_noCFI c: get_code_nature c <> IsCFI -> - to_bblock_exit c = (b, c0) -> - c = c0. + to_bblock_exit c = (None, c). Proof. - intros H1 H2. destruct c as [|i c]. - - simpl in H2; inversion H2; auto. - - destruct i; unfold to_bblock_header in H2; inversion H2; auto; - simpl in H1; contradict H1; auto. + intros H. destruct c as [|i c]; simpl; auto. + destruct i; simpl; auto. + all: contradict H; simpl; auto. Qed. Lemma to_bblock_exit_wf c b c0: @@ -270,7 +264,7 @@ Proof. intros H; inversion H; subst; clear H; simpl; auto. Qed. -Lemma to_bblock_basic_inst_then_label i c bi: +Lemma to_bblock_basic_then_label i c bi: get_code_nature (i::c) = IsBasicInst -> get_code_nature c = IsLabel -> to_basic_inst i = Some bi -> @@ -282,19 +276,17 @@ Proof. destruct i; simpl in *; inversion H3; subst; auto. Qed. -Lemma to_bblock_cf_inst_then_label i c cfi: +Lemma to_bblock_CFI i c cfi: get_code_nature (i::c) = IsCFI -> - get_code_nature c = IsLabel -> to_cfi i = Some cfi -> fst (to_bblock (i::c)) = {| header := nil; body := nil; exit := Some cfi |}. Proof. - intros H1 H2 H3. - destruct c as [|i' c]; try (contradict H1; simpl; discriminate). - destruct i'; try (contradict H1; simpl; discriminate). - destruct i; simpl in *; inversion H3; subst; auto. + intros H1 H2. + destruct i; try discriminate. + all: subst; rewrite <- H2; simpl; auto. Qed. -Lemma to_bblock_no_label c: +Lemma to_bblock_noLabel c: get_code_nature c <> IsLabel -> fst (to_bblock c) = {| header := nil; @@ -349,26 +341,7 @@ Proof. intros H; inversion H; subst; clear H; simpl; auto. Qed. -(* -Lemma to_bblock_label_then_nil b l c c': - to_bblock (Mlabel l :: c) = (b, c') -> - body b = nil -> - exit b = None -> - c = c'. -Proof. - intros TOB BB EB. - unfold to_bblock in TOB. - remember (to_bblock_header _) as tbh; destruct tbh as [h c0]. - remember (to_bblock_body _) as tbb; destruct tbb as [bdy c1]. - remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2]. - inversion TOB; subst. simpl in *. clear TOB. - inversion Heqtbh; subst. clear Heqtbh. - exploit to_bblock_body_nil; eauto. intros; subst. clear Heqtbb. - exploit to_bblock_exit_nil; eauto. -Qed. -*) - -Lemma to_bblock_basic_inst c i bi: +Lemma to_bblock_basic c i bi: get_code_nature (i::c) = IsBasicInst -> to_basic_inst i = Some bi -> get_code_nature c <> IsLabel -> @@ -383,40 +356,41 @@ Proof. apply bblock_eq; simpl. (* header *) + destruct i; simpl; auto; ( - exploit to_bblock_no_label; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]). + exploit to_bblock_noLabel; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]). (* body *) (* FIXME - the proof takes some time to prove.. N² complexity :( *) - + destruct i; inversion H0; try ( - destruct i0; try ( - subst; unfold to_bblock; - remember (to_bblock_header _) as tbh; destruct tbh; - remember (to_bblock_header (_::c)) as tbh'; destruct tbh'; - inversion Heqtbh; inversion Heqtbh'; subst; - - remember (to_bblock_body _) as tbb; destruct tbb; - remember (to_bblock_body (_::c)) as tbb'; destruct tbb'; - inversion Heqtbb; inversion Heqtbb'; destruct (to_bblock_body c); - inversion H3; inversion H4; subst; - - remember (to_bblock_exit _) as tbc; destruct tbc; - simpl; auto ); - contradict H1; simpl; auto ). -(* exit - same as body *) - + destruct i; inversion H0; try ( - destruct i0; try ( - subst; unfold to_bblock; - remember (to_bblock_header _) as tbh; destruct tbh; - remember (to_bblock_header (_::c)) as tbh'; destruct tbh'; - inversion Heqtbh; inversion Heqtbh'; subst; - - remember (to_bblock_body _) as tbb; destruct tbb; - remember (to_bblock_body (_::c)) as tbb'; destruct tbb'; - inversion Heqtbb; inversion Heqtbb'; destruct (to_bblock_body c); - inversion H3; inversion H4; subst; - - remember (to_bblock_exit _) as tbc; destruct tbc; - simpl; auto ); - contradict H1; simpl; auto ). + + unfold to_bblock. + remember (to_bblock_header _) as tbh; destruct tbh. + remember (to_bblock_body _) as tbb; destruct tbb. + remember (to_bblock_exit _) as tbe; destruct tbe. + simpl. + destruct i; destruct i0. + all: try (simpl in H1; contradiction). + all: try discriminate. + all: try ( + simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst; + simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc; + inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1; + inversion H0; clear H0; subst; destruct (to_bblock_body c); + inversion Heqtbbc; clear Heqtbbc; subst; + destruct (to_bblock_exit c1); simpl; auto; fail). +(* exit *) + + unfold to_bblock. + remember (to_bblock_header _) as tbh; destruct tbh. + remember (to_bblock_body _) as tbb; destruct tbb. + remember (to_bblock_exit _) as tbe; destruct tbe. + simpl. + destruct i; destruct i0. + all: try (simpl in H1; contradiction). + all: try discriminate. + all: try ( + simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst; + simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc; + inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1; + inversion H0; clear H0; subst; destruct (to_bblock_body c) eqn:TBBC; + inversion Heqtbbc; clear Heqtbbc; subst; + destruct (to_bblock_exit c1) eqn:TBBE; simpl; + inversion Heqtbe; clear Heqtbe; subst; auto; fail). Qed. Lemma to_bblock_size_single_label c i: @@ -439,7 +413,7 @@ Proof. intros; rewrite to_bblock_size_single_label; auto. Qed. -Lemma to_bblock_size_basicinst_neqz c: +Lemma to_bblock_size_basic_neqz c: get_code_nature c = IsBasicInst -> size (fst (to_bblock c)) <> 0%nat. Proof. @@ -448,12 +422,12 @@ Proof. ( destruct (get_code_nature c) eqn:gcnc; (* Case gcnc is not IsLabel *) - try (erewrite to_bblock_basic_inst; eauto; [ + try (erewrite to_bblock_basic; eauto; [ unfold size; simpl; auto | simpl; auto | rewrite gcnc; discriminate ]); - erewrite to_bblock_basic_inst_then_label; eauto; [ + erewrite to_bblock_basic_then_label; eauto; [ unfold size; simpl; auto | simpl; auto ] @@ -468,18 +442,18 @@ Proof. destruct i; discriminate. Qed. -Lemma to_bblock_size_single_basicinst c i: +Lemma to_bblock_size_single_basic c i: get_code_nature (i::c) = IsBasicInst -> get_code_nature c <> IsLabel -> size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))). Proof. intros. destruct i; try (contradict H; simpl; discriminate); try ( - (exploit to_bblock_basic_inst; eauto); + (exploit to_bblock_basic; eauto); [remember (to_basic_inst _) as tbi; destruct tbi; eauto |]; intro; rewrite H1; unfold size; simpl; assert ((length (header (fst (to_bblock c)))) = 0%nat); - exploit to_bblock_no_label; eauto; intro; rewrite H2; simpl; auto; + exploit to_bblock_noLabel; eauto; intro; rewrite H2; simpl; auto; rewrite H2; auto ). Qed. @@ -505,87 +479,37 @@ Proof. destruct p3 as [h3 c3]. exploit to_bblock_exit_wfe; eauto. inversion H0. omega. - - exploit to_bblock_header_eq; eauto. rewrite <- Heqgcn. discriminate. - intro; subst. - remember (to_bblock_body c1) as p2; eauto. + - exploit to_bblock_header_noLabel; eauto. rewrite <- Heqgcn. discriminate. + intro. rewrite H1 in Heqp1. inversion Heqp1. clear Heqp1. subst. + remember (to_bblock_body c) as p2; eauto. destruct p2 as [h2 c2]. exploit to_bblock_body_wf; eauto. remember (to_bblock_exit c2) as p3; eauto. destruct p3 as [h3 c3]. exploit to_bblock_exit_wfe; eauto. inversion H0. omega. - - exploit to_bblock_header_eq; eauto. rewrite <- Heqgcn. discriminate. - intro; subst. - remember (to_bblock_body c1) as p2; eauto. + - exploit to_bblock_header_noLabel; eauto. rewrite <- Heqgcn. discriminate. + intro. rewrite H1 in Heqp1. inversion Heqp1; clear Heqp1; subst. + remember (to_bblock_body c) as p2; eauto. destruct p2 as [h2 c2]. - exploit (to_bblock_body_eq c1 h2 c2); eauto. rewrite <- Heqgcn. discriminate. - intro; subst. - remember (to_bblock_exit c2) as p3; eauto. + exploit (to_bblock_body_noBasic c); eauto. rewrite <- Heqgcn. discriminate. + intros H2; rewrite H2 in Heqp2; inversion Heqp2; clear Heqp2; subst. + remember (to_bblock_exit c) as p3; eauto. destruct p3 as [h3 c3]. - exploit (to_bblock_exit_wf c2 h3 c3); eauto. + exploit (to_bblock_exit_wf c h3 c3); eauto. inversion H0. omega. Qed. -Lemma to_bblock_nonil c i c0: - c = i :: c0 -> - size (fst (to_bblock c)) <> 0%nat. +Lemma to_bblock_nonil i c0: + size (fst (to_bblock (i :: c0))) <> 0%nat. Proof. - intros H. remember (get_code_nature c) as gcnc. destruct gcnc. + intros H. remember (i::c0) as c. remember (get_code_nature c) as gcnc. destruct gcnc. - contradict Heqgcnc. subst. simpl. destruct i; discriminate. - - eapply to_bblock_size_label_neqz; auto. - - eapply to_bblock_size_basicinst_neqz; auto. - - eapply to_bblock_size_cfi_neqz; auto. + - eapply to_bblock_size_label_neqz; eauto. + - eapply to_bblock_size_basic_neqz; eauto. + - eapply to_bblock_size_cfi_neqz; eauto. Qed. -(* -Lemma to_bblock_islabel c l: - is_label l (fst (to_bblock (Mlabel l :: c))) = true. -Proof. - unfold to_bblock. - remember (to_bblock_header _) as tbh; destruct tbh as [h c0]. - remember (to_bblock_body _) as tbc; destruct tbc as [bdy c1]. - remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2]. - simpl. inversion Heqtbh. unfold is_label. simpl. - apply peq_true. -Qed. - -Lemma body_fst_to_bblock_label l c: - body (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_body c). -Proof. - destruct c as [|i c']; simpl; auto. - destruct i; simpl; auto. - all: ( - remember (to_bblock_body c') as tbbc; destruct tbbc as [tc c'']; simpl; - unfold to_bblock; - remember (to_bblock_header _) as tbh; destruct tbh as [h c0]; - remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1]; - remember (to_bblock_exit c1) as tbe; destruct tbe as [ext c2]; - simpl; simpl in Heqtbh; inversion Heqtbh; subst c0; - simpl in Heqtbc; remember (to_bblock_body c') as tbc'; destruct tbc' as [tc' osef]; - inversion Heqtbc; inversion Heqtbbc; auto - ). -Qed. - -Lemma exit_fst_to_bblock_label c c' l: - snd (to_bblock_body c) = c' -> - exit (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_exit c'). -Proof. - intros H. destruct c as [|i c]; [simpl in *; subst; auto |]. - unfold to_bblock. - remember (to_bblock_header _) as tbh; destruct tbh as [h c0]. - remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1]. - remember (to_bblock_exit c1) as tbe; destruct tbe as [ext c2]. - simpl in *. inversion Heqtbh; subst. - destruct (to_basic_inst i) eqn:TBI. - - remember (to_bblock_body c) as tbbc; destruct tbbc as [p c'']. - simpl. simpl in Heqtbc. rewrite TBI in Heqtbc. rewrite <- Heqtbbc in Heqtbc. - inversion Heqtbc; subst. apply (f_equal fst) in Heqtbe; auto. - - simpl. simpl in Heqtbc. rewrite TBI in Heqtbc. - inversion Heqtbc; subst. clear Heqtbh Heqtbc. unfold to_bblock_exit in Heqtbe. - apply (f_equal fst) in Heqtbe; auto. -Qed. -*) - Function trans_code (c: Mach.code) { measure length c }: code := match c with | nil => nil diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 0efd4586..62391792 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -328,7 +328,7 @@ Ltac ExploitDistEndBlockCode := | [ H : dist_end_block_code (Mlabel ?l :: ?c) <> 0%nat |- _ ] => exploit (to_bblock_size_single_label c (Mlabel l)); eauto | [ H : dist_end_block_code (?i0 :: ?c) <> 0%nat |- _ ] => - exploit (to_bblock_size_single_basicinst c i0); eauto + exploit (to_bblock_size_single_basic c i0); eauto | _ => idtac end. @@ -339,45 +339,44 @@ Ltac totologize H := assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert) end. -(* FIXME - refactoriser avec get_code_nature pour que ce soit plus joli *) Lemma dist_end_block_code_simu_mid_block i c: dist_end_block_code (i::c) <> 0 -> (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)). Proof. intros H. - remember (get_code_nature c) as gcnc; destruct gcnc. - (* when c is nil *) - - contradict H; rewrite get_code_nature_nil_contra with (c := c); auto. destruct i; simpl; auto. - (* when c is IsLabel *) - - remember i as i0; remember (to_basic_inst i) as sbi; remember (to_cfi i) as scfi; - remember (get_code_nature (i::c)) as gcnic; - destruct i. - (* when i is a basic instruction *) - 1-6: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_basic_inst_then_label; eauto; - [ totologize Heqgcnic; eapply Htoto - | totologize Heqsbi; try eapply Htoto - | intro; subst; rewrite H; simpl; auto - ] ); fail). - (* when i is a control flow instruction *) - 1-8: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_cf_inst_then_label; eauto; - [ totologize Heqgcnic; eapply Htoto - | totologize Heqscfi; try eapply Htoto - | intro; subst; rewrite H; simpl; auto - ] ); fail). - (* when i is a label *) - unfold dist_end_block_code in * |- *. subst i0. - rewrite (to_bblock_size_single_label c (Mlabel l)) in * |- *; simpl in * |- *; auto. omega. - (* when c is IsBasicInst or IsCFI *) - -(* - - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) - ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | - unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). - - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) - ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | - unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). -*) -Admitted. + unfold dist_end_block_code. + destruct (get_code_nature (i::c)) eqn:GCNIC. + - apply get_code_nature_empty in GCNIC. discriminate. + - rewrite to_bblock_size_single_label; auto. + destruct c as [|i' c]. + + contradict H. destruct i; simpl; auto. + + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. omega. + - destruct (get_code_nature c) eqn:GCNC. + + apply get_code_nature_empty in GCNC. subst. contradict H. destruct i; simpl; auto. + + contradict H. destruct c as [|i' c]; try discriminate. + destruct i'; try discriminate. + destruct i; try discriminate. all: simpl; auto. + + destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate]. + erewrite to_bblock_basic; eauto; [| rewrite GCNC; discriminate ]. + simpl. destruct c as [|i' c]; try discriminate. + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. + cutrewrite (Datatypes.S (size (fst (to_bblock (i'::c))) - 1) = size (fst (to_bblock (i'::c)))). + unfold size. cutrewrite (length (header (fst (to_bblock (i' :: c)))) = 0). simpl. omega. + rewrite to_bblock_noLabel. simpl; auto. + rewrite GCNC. discriminate. + omega. + + destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate]. + erewrite to_bblock_basic; eauto; [| rewrite GCNC; discriminate ]. + simpl. destruct c as [|i' c]; try discriminate. + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. + cutrewrite (Datatypes.S (size (fst (to_bblock (i'::c))) - 1) = size (fst (to_bblock (i'::c)))). + unfold size. cutrewrite (length (header (fst (to_bblock (i' :: c)))) = 0). simpl. omega. + rewrite to_bblock_noLabel. simpl; auto. + rewrite GCNC. discriminate. + omega. + - contradict H. destruct i; try discriminate. + all: unfold dist_end_block_code; erewrite to_bblock_CFI; eauto; simpl; eauto. +Qed. Local Hint Resolve dist_end_block_code_simu_mid_block. @@ -543,7 +542,7 @@ Proof. assert (X: Datatypes.S (dist_end_block_code c0) = (size (fst (to_bblock c0)))). { unfold dist_end_block_code. remember (size _) as siz. - assert (siz <> 0%nat). rewrite Heqsiz; apply to_bblock_nonil with (c0 := c) (i := i) (c := c0); auto. + assert (siz <> 0%nat). rewrite Heqsiz; subst; apply to_bblock_nonil with (c0 := c) (i := i); auto. omega. } |