proposition: Lemma valid_check_roweq lres : C.valid rho (check_roweq lres).
proof: Proof. unfold check_roweq. case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a Heq2. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq3; try (intros; now apply C.interp_true). case_eq (t_atom .[ a1]); try (intros; now apply C.interp_true). intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq4; try (intros; now apply C.interp_true). case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true). intros [ ] c1 c2 c3 Heq5. - case_eq (Typ.eqb t0 t2 && Typ.eqb t t1 && Typ.eqb t t3 && (b2 =? c2) && (a2 =? c3)); simpl; intros Heq6; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq. unfold Var.interp. rewrite wf_interp_form; trivial. rewrite Heq2. simpl. rewrite !andb_true_iff in Heq6. destruct Heq6 as ((((Heq6a, Heq6b), Heq6c), Heq6d), Heq6e). apply Typ.eqb_spec in Heq6a. apply Typ.eqb_spec in Heq6b. apply Typ.eqb_spec in Heq6c. apply Int63.eqb_spec in Heq6d. apply Int63.eqb_spec in Heq6e. pose proof (rho_interp (Lit.blit lres)) as Hrho. rewrite Heq2 in Hrho. simpl in Hrho. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. pose proof (H a). assert (a <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. specialize (H0 H1). simpl in H0. rewrite Heq3 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. unfold get_type' in H2, H3, H0. unfold v_type in H2, H3, H0. case_eq (t_interp .[ a]). intros v_typea v_vala Htia. rewrite Htia in H0. case_eq v_typea; intros; rewrite H4 in H0; try now contradict H0. case_eq (t_interp .[ a1]). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H3. case_eq (t_interp .[ a2]). intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H2. rewrite Atom.t_interp_wf in Htia; trivial. rewrite Atom.t_interp_wf in Htia1; trivial. rewrite Atom.t_interp_wf in Htia2; trivial. rewrite Heq3 in Htia. simpl in Htia. rewrite !Atom.t_interp_wf in Htia; trivial. rewrite Htia1, Htia2 in Htia. simpl in Htia. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. generalize dependent v_vala1. generalize dependent v_vala2. generalize dependent v_vala. rewrite H2, H3, H4. rewrite !Typ.cast_refl. intros. simpl in Htia. unfold Bval in Htia. specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t v_vala1 v_vala2) (v_vala)). intros. specialize (H5 Htia). pose proof (H a1). assert (a1 <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4. easy. specialize (H6 H7). simpl in H6. rewrite Heq4 in H6. simpl in H6. rewrite !andb_true_iff in H6. destruct H6 as ((H6a, H6b), H6c). apply Typ.eqb_spec in H6a. apply Typ.eqb_spec in H6b. apply Typ.eqb_spec in H6c. pose proof (H b1). assert (b1 <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq5. easy. specialize (H6 H8). simpl in H6. rewrite Heq5 in H6. simpl in H6. rewrite !andb_true_iff in H6. destruct H6 as (((H6d, H6e), H6f), H6h). apply Typ.eqb_spec in H6e. apply Typ.eqb_spec in H6f. apply Typ.eqb_spec in H6h. unfold get_type' in H6b, H6c, H6d. unfold v_type in H6b, H6c, H6d. case_eq (t_interp .[ b2]). intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H6c. rewrite Atom.t_interp_wf in Htib2; trivial. case_eq (t_interp .[ b1]). intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H6d. rewrite Atom.t_interp_wf in Htib1; trivial. rewrite <- Heq6d, <- Heq6e in *. rewrite Heq5 in Htib1. simpl in Htib1. generalize dependent v_valb2. rewrite H6c. intros. unfold Atom.interp_form_hatom, interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Heq3. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Heq4, Htia2. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Heq5, Htib2. simpl. rewrite Htib1. simpl. rewrite Typ.cast_refl. unfold apply_binop. rewrite Typ.cast_refl. case_eq (t_interp .[ b1]); intros. pose proof H6. rewrite H6 in H6b. rewrite !Atom.t_interp_wf in H6; trivial. rewrite Heq5 in H6. simpl in H6. rewrite H6 in Htib1. inversion Htib1. generalize dependent v_val0. rewrite H6b. intros. rewrite Typ.cast_refl. simpl. unfold get_type' in H6a. unfold v_type in H6a. case_eq (t_interp .[ a1]). intros. rewrite H10 in H6a. rewrite !Atom.t_interp_wf in H10; trivial. rewrite H10 in Htia1. inversion Htia1. rewrite <- H6a in H14. generalize dependent v_val0. rewrite H14. intros. rewrite Typ.cast_refl. simpl. unfold apply_terop in H6. unfold get_type', v_type in H6e, H6f, H6h. case_eq ( t_interp .[ c1]); intros. rewrite H13 in H6e. rewrite H13 in H6. case_eq (t_interp .[ b2]); intros. rewrite H16 in H6f. rewrite H16 in H6. case_eq (t_interp .[ a2]); intros. rewrite H17 in H6h. rewrite H17 in H6. generalize dependent v_val2. generalize dependent v_val3. generalize dependent v_val4. rewrite H6e, H6f, H6h. rewrite !Typ.cast_refl. intros. unfold Bval in H6. rewrite <- H11 in H6d. rewrite H6b in H6d. rewrite andb_true_iff in H6d. destruct H6d as (H6d1, H6d2). apply Typ.eqb_spec in H6d1. apply Typ.eqb_spec in H6d2. generalize dependent v_val2. generalize dependent v_val3. generalize dependent v_val4. rewrite H6d1, H6d2, H14. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) (@store _ _ (Typ.dec_interp t_i t0) _ _ _ (Typ.comp_interp t_i t) _ v_val2 v_val3 v_val4) v_val0). intros. specialize (H18 H6). rewrite <- H18. rewrite !Atom.t_interp_wf in H16; trivial. rewrite H16 in Htib2. specialize (Atom.Bval_inj2 t_i t0 v_val3 v_valb2). intros. specialize (H19 Htib2). rewrite <- H19. rewrite !Atom.t_interp_wf in H17; trivial. rewrite H17 in Htia2. specialize (Atom.Bval_inj2 t_i t v_val4 v_vala2). intros. specialize (H20 Htia2). rewrite <- H20. apply Typ.i_eqb_spec. apply (read_over_write (elt_dec:=(@EqbToDecType _ (@Eqb _ (projT2 (Typ.interp_compdec_aux t_i _)))))). Qed.
imports: Bool List Int63 PArray Psatz ZArith Misc State SMT_terms FArray SMT_classes