proposition: Lemma erase_correct k min (f : recalg k) v n c : (ra_bs_c min c f v n <-> eval c min (erase f) (vec_list v) = Some (inl n)).
proof: Proof. revert k min f v n. pattern c. eapply lt_wf_ind. intros. destruct f; cbn. - split. + inversion 1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H4. subst. reflexivity. + destruct n; inversion 1. subst. econstructor. - split. + inversion 1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H3. subst. reflexivity. + destruct n; inversion 1. subst. econstructor. - split. + inversion 1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H3. subst. cbn; revert H0; vec split v with x; auto. + destruct n; inversion 1. revert H0 H2; vec split v with x; cbn. intros [=] _; subst; constructor. - split. + inversion 1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H5. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H6. subst. cbn. rewrite vec_list_nth. reflexivity. + destruct n; inversion 1. rewrite vec_list_nth in H2. inv H2. econstructor. - split. + inversion 1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H2. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H7. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H7. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H8. subst. assert (forall j : pos k, eval (c0 - pos2nat j) min (erase (vec_pos t j)) (vec_list v) = Some (inl (vec_pos w j))). { intros. eapply H. 1: lia. cbn. eapply H. 1: lia. eapply H. 1: lia. specialize (H9 j). eapply H in H9. 2:lia. eapply H. 1: lia. eauto. } remember (S c0) as c'. cbn. assert (eval c' min (rec_erase erase t) (vec_list v) = Some (inr (vec_list w))). { subst. clear - H1. revert c0 H1. induction t; intros. - cbn; vec nil w; reflexivity. - cbn. pose proof (H1 pos_fst). cbn in H. rewrite pos2nat_fst in H. replace (c0 - 0) with c0 in H by lia. rewrite H. revert H1 H; vec split w with y; intros H1 H. destruct c0. 1: cbn in H. 1: inv H. erewrite IHt. 1: reflexivity. intros. specialize (H1 (pos_nxt j)). rewrite pos2nat_nxt in H1. eassumption. } rewrite H2. subst. eapply H in H10. 1: rewrite H10. 1: reflexivity. lia. + destruct n; inversion 1. destruct (eval n min (rec_erase erase t) (vec_list v)) eqn:E; try congruence. destruct s; try congruence. destruct (eval n min (erase f) l) eqn:E2; try congruence. destruct s; try congruence. inv H2. destruct n; try now inv E2. destruct (list_vec_full l). destruct (eval_inv E) as (w & ? & ?). subst. eapply in_ra_bs_c_comp with (w := w). * intros. eapply H. 1: lia. specialize (H2 j). assert (S n - S (pos2nat j) = n - pos2nat j) by lia. rewrite H1 in *. eauto. * eapply H. 1: lia. eassumption. - split. 1: inversion 1. + eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H4. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H6. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H7. subst. cbn. eapply H in H8. 2:lia. rewrite H8. reflexivity. + eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H2. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H5. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H6. subst. eapply H in H7. 1: cbn. 2:lia. cbn in H7. rewrite H7. eapply H in H9. 2:lia. cbn in H9. rewrite H9. reflexivity. + intros. destruct n; inv H0. revert H2; vec split v with n1; cbn; intros H2. destruct n1. * destruct (eval n min (erase f1) (vec_list v)) eqn:E. 1: destruct s; inv H2. -- econstructor. eapply H. 1: lia. eauto. -- econstructor. congruence. * destruct eval eqn:E2; try congruence. destruct s; try congruence. destruct (eval n min (erase f2)) eqn:E3. 1: destruct s; inv H2. -- econstructor. 1: eapply H. 1: lia. 1: eauto. eapply H. 1: lia. eauto. -- congruence. - split. + inversion 1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H1. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H2. subst. clear H0. unfold ge in *. revert c0 H w H7 H8. pattern n0. revert min H3. eapply le_ind2; intros. * cbn in *. eapply H in H8. 2:lia. assert (c0 - (n0 - n0) = c0) by lia. rewrite H0 in *. cbn in H8. rewrite H8. reflexivity. * destruct n0; try lia. assert (n < S n0) by lia. assert (H10 := H7). specialize (H7 (nat2pos H2)). rewrite pos2nat_nat2pos in H7. assert (n <= n) by lia. eapply H7 in H3. eapply H1 in H3. 2: lia. cbn. assert (c0 - (n - n) = c0) by lia. rewrite H4 in *. cbn in H3. rewrite H3. assert (eval c0 (S n) (rc_min (erase f)) (vec_list v) = Some (inl (S n0))). { eapply H1 with (f := ra_min f). 1: lia. destruct c0. 1: inv H3. econstructor. 1: lia. - intros ? ?. specialize (H10 j). assert (S c0 - (pos2nat j - n) = c0 - (pos2nat j - S n)) by lia. rewrite H6 in *. eapply H10. lia. - assert (S c0 - (S n0 - n) = c0 - (S n0 - S n)) by lia. rewrite H5 in *. eassumption. } now rewrite H5. + intros. destruct n; try now inv H0. cbn in H0. destruct (eval n) eqn:E1; try now inv H0. destruct s; try congruence. destruct n1; inv H0. * econstructor. 1: lia. -- intros. pose proof (pos2nat_prop j). lia. -- eapply H. 1:lia. assert (n - (n0 - n0) = n) as -> by lia. eassumption. * destruct (eval n (S min)) eqn:E2; try now inv H2. destruct s; inv H2. eapply H with (f := ra_min f) in E2. 2:lia. eapply H with (v := vec_cons min v) in E1. 2:lia. inversion E2; subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H0. subst. eapply (Eqdep_dec.inj_pair2_eq_dec _ nat_eq_dec) in H1. subst. assert (min < n0) by lia. eapply in_ra_bs_c_min with (w := vec_change w (nat2pos H0) n1). -- lia. -- intros. inversion H1. ++ subst. rewrite nat2pos_pos2nat. rewrite vec_change_eq. 2:reflexivity. assert (S c0 - (pos2nat j - pos2nat j) = S c0) as -> by lia. eassumption. ++ specialize (H6 j). assert (S c0 - (S m - min) = c0 - (pos2nat j - S min)) by lia. rewrite H5 in *. enough (vec_pos w j = vec_pos (vec_change w (nat2pos H0) n1) j). { rewrite H8 in H6. rewrite H3. eapply H6. lia. } assert (pos2nat j > min) by lia. eapply vec_pos_gt. rewrite pos2nat_nat2pos. lia. -- assert (S c0 - (n0 - min) = c0 - (n0 - S min)) by lia. rewrite H1. eassumption. Unshelve. exact vec_zero. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract