proposition: Lemma valid_check_rowneq cl : C.valid rho (check_rowneq cl).
proof: Proof. unfold check_rowneq. case_eq (cl); [ intros | intros i l ]; simpl; try now apply C.interp_true. case_eq (l); [ intros | intros j xsl ]; simpl; try now apply C.interp_true. case_eq (xsl); intros; simpl; try now apply C.interp_true. case_eq (Lit.is_pos i); intro Heq; simpl; try now apply C.interp_true. case_eq (Lit.is_pos j); intro Heq2; simpl; try now apply C.interp_true. case_eq (t_form .[ Lit.blit i]); try (intros; now apply C.interp_true). intros a Heq3. case_eq (t_form .[ Lit.blit j]); try (intros; now apply C.interp_true). intros b Heq4. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq5; try (intros; now apply C.interp_true). case_eq (t_atom .[ b]); try (intros; now apply C.interp_true). intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq6; try (intros; now apply C.interp_true). case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true). intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq7; try (intros; now apply C.interp_true). case_eq (t_atom .[ b2]); try (intros; now apply C.interp_true). intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq8; try (intros; now apply C.interp_true). case_eq (Typ.eqb t t1 && Typ.eqb t t3 && Typ.eqb t0 t2 && Typ.eqb t0 t4); try (intros; now apply C.interp_true). intros Heq9. rewrite !andb_true_iff in Heq9. destruct Heq9 as (((Heq9a, Heq9b), Heq9c), Heq9d). apply Typ.eqb_spec in Heq9a. apply Typ.eqb_spec in Heq9b. apply Typ.eqb_spec in Heq9c. apply Typ.eqb_spec in Heq9d. subst t1 t2 t3 t4. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. assert (H15: b1 <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. discriminate. assert (H20: b2 <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq8. discriminate. assert (H9: b <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. discriminate. assert (H3: a <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq5. discriminate. apply H2 in H15. apply H2 in H20. apply H2 in H3. apply H2 in H9. rewrite Heq7 in H15. rewrite Heq8 in H20. rewrite Heq6 in H9. rewrite Heq5 in H3. simpl in H15, H20, H3, H9. rewrite !andb_true_iff in H15, H20, H3, H9. destruct H3 as ((H3, H6), H5). destruct H9 as ((H9, H12), H11). destruct H15 as ((H15, H18), H17). destruct H20 as ((H20, H23), H22). unfold get_type', v_type in H3, H5, H6, H9, H11, H12, H15, H17, H18, H20, H22, H23. case_eq (t_interp .[ a]). intros v_typea v_vala Htia. rewrite Htia in H3. case_eq v_typea; intros; rewrite H4 in H3; try now contradict H3. case_eq (t_interp .[ a1]). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H6. case_eq (t_interp .[ a2]). intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H5. rewrite Atom.t_interp_wf in Htia, Htia1, Htia2; trivial. rewrite Heq5 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 H5. apply Typ.eqb_spec in H6. generalize dependent v_vala1. generalize dependent v_vala2. generalize dependent v_vala. rewrite H5, H6, 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 H8. specialize (H8 Htia). case_eq (t_interp .[ b]). intros v_typeb v_valb Htib. rewrite Htib in H9; case_eq v_typeb; intros; rewrite H7 in H9; try now contradict H9. case_eq (t_interp .[ b1]). intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H12. case_eq (t_interp .[ b2]). intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H11. rewrite Atom.t_interp_wf in Htib, Htib1, Htib2; trivial. rewrite Heq6 in Htib. simpl in Htib. rewrite !Atom.t_interp_wf in Htib; trivial. rewrite Htib1, Htib2 in Htib. simpl in Htib. apply Typ.eqb_spec in H11. apply Typ.eqb_spec in H12. generalize dependent v_valb1. generalize dependent v_valb2. generalize dependent v_valb. rewrite H11, H12, H7. rewrite !Typ.cast_refl. intros. simpl in Htib. unfold Bval in Htib. specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t0 v_valb1 v_valb2) (v_valb)). intros H14. specialize (H14 Htib). case_eq (t_interp .[ b1]). intros v_typeb1' v_valb1' Htib1'. rewrite Htib1' in H15. case_eq (t_interp .[ c1]). intros v_typec1 v_valc1 Htic1. rewrite Htic1 in H18. case_eq (t_interp .[ c2]). pose proof Htib1' as Htib1''. intros v_typec2 v_valc2 Htic2. rewrite Htic2 in H17. pose proof Htic2 as Htic2''. rewrite Atom.t_interp_wf in Htib1', Htic1, Htic2; trivial. rewrite Heq7 in Htib1'. simpl in Htib1'. rewrite !Atom.t_interp_wf in Htib1'; trivial. rewrite Htic1, Htic2 in Htib1'. simpl in Htib1'. apply Typ.eqb_spec in H17. apply Typ.eqb_spec in H18. apply Typ.eqb_spec in H15. generalize dependent v_valc1. generalize dependent v_valc2. generalize dependent v_valb1'. rewrite H17, H18. rewrite !Typ.cast_refl. intros. simpl in Htib1'. unfold Bval in Htib1'. generalize dependent v_valc1. generalize dependent v_valc2. generalize dependent v_valb1'. rewrite H15. intros. specialize (Atom.Bval_inj2 t_i (v_typeb1') (select v_valc1 v_valc2) (v_valb1')). intro H19. specialize (H19 Htib1'). case_eq (t_interp .[ b2]). intros v_typeb2' v_valb2' Htib2'. rewrite Htib2' in H20. case_eq (t_interp .[ d1]). intros v_typed1 v_vald1 Htid1. rewrite Htid1 in H23. case_eq (t_interp .[ d2]). pose proof Htib2' as Htib2''. intros v_typed2 v_vald2 Htid2. rewrite Htid2 in H22. rewrite Atom.t_interp_wf in Htib2', Htid1, Htid2; trivial. rewrite Heq8 in Htib2'. simpl in Htib2'. rewrite !Atom.t_interp_wf in Htib2'; trivial. rewrite Htid1, Htid2 in Htib2'. simpl in Htib2'. apply Typ.eqb_spec in H22. apply Typ.eqb_spec in H23. apply Typ.eqb_spec in H20. generalize dependent v_vald1. generalize dependent v_vald2. generalize dependent v_valb2'. rewrite H22, H23. rewrite !Typ.cast_refl. intros. simpl in Htib2'. unfold Bval in Htib2'. generalize dependent v_vald1. generalize dependent v_vald2. generalize dependent v_valb2'. rewrite H20. intros. specialize (Atom.Bval_inj2 t_i (v_typeb2') (select v_vald1 v_vald2) (v_valb2')). intro H24. specialize (H24 Htib2'). case_eq (store_of_me c1 d1); case_eq (store_of_me d1 c1); try (intros; try(destruct p0, p0); now apply C.interp_true). - unfold store_of_me. intro HT1. clear HT1. case_eq (t_atom .[ d1]); try discriminate. intros [ t5 t6 ] e1 e2 e3 Heq10 [[ti3 te3] i1]. case_eq (e1 =? c1); try discriminate. intros Heq11c. intro HT. injection HT. intros. subst i1 te3 ti3. clear HT. case_eq ( Typ.eqb t t5 && Typ.eqb v_typeb1' t6 && ((e2 =? a1) && (c2 =? a2) && (d2 =? a2) || (e2 =? a2) && (c2 =? a1) && (d2 =? a1))); simpl; intros Heq11; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. case_eq (Lit.interp rho i). intros isit. easy. intros isif. rewrite orb_false_l. specialize (rho_interp ( Lit.blit i)). rewrite Heq3 in rho_interp. simpl in rho_interp. unfold Lit.interp in isif. rewrite Heq in isif. unfold Var.interp in isif. rewrite rho_interp in isif. unfold Atom.interp_form_hatom, interp_hatom in isif. rewrite Atom.t_interp_wf in isif; trivial. rewrite Heq5 in isif. simpl in isif. unfold interp_bool in isif. unfold Lit.interp. rewrite Heq2. unfold Var.interp. rewrite !wf_interp_form; trivial. rewrite Heq4. simpl. rewrite !andb_true_iff in Heq11. destruct Heq11 as ((Heq11a, Heq11b), Heq11d). rewrite !orb_true_iff in Heq11d. apply Typ.eqb_spec in Heq11a. apply Typ.eqb_spec in Heq11b. apply Int63.eqb_spec in Heq11c. rewrite !andb_true_iff in Heq11d. rewrite !Int63.eqb_spec in Heq11d. rewrite !Atom.t_interp_wf in isif; trivial. rewrite Htia1, Htia2 in isif. simpl in isif. unfold Bval in isif. assert (H25: d1 <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq10. discriminate. apply H2 in H25. rewrite Heq10 in H25. simpl in H25. rewrite !andb_true_iff in H25. destruct H25 as (((H25, H29), H28), H27). unfold get_type', v_type in H25, H27, H28, H29. case_eq (t_interp .[ d1]). intros v_typed1' v_vald1' Htid1'. rewrite Htid1' in H25. case_eq v_typed1'; intros; rewrite H10 in H25; try now contradict H25. rewrite andb_true_iff in H25; destruct H25 as (H25a, H25b). case_eq (t_interp .[ e1]). intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H29. case_eq (t_interp .[ e2]). intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H28. case_eq (t_interp .[ e3]). intros v_typee3 v_vale3 Htie3. rewrite Htie3 in H27. pose proof Htid1' as Htid1''. rewrite Atom.t_interp_wf in Htid1', Htie1, Htie2, Htie3; trivial. rewrite Heq10 in Htid1'. simpl in Htid1'. rewrite !Atom.t_interp_wf in Htid1'; trivial. rewrite Htie1, Htie2, Htie3 in Htid1'. simpl in Htid1'. apply Typ.eqb_spec in H25a. apply Typ.eqb_spec in H25b. apply Typ.eqb_spec in H27. apply Typ.eqb_spec in H28. apply Typ.eqb_spec in H29. generalize dependent v_vale1. generalize dependent v_vale2. generalize dependent v_vale3. generalize dependent v_vald1'. rewrite H27, H28, H29. rewrite !Typ.cast_refl. intros. simpl in Htid1'. unfold Bval in Htid1'. generalize dependent v_vale1. generalize dependent v_vale2. generalize dependent v_vale3. generalize dependent v_vald1'. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (@store _ _ (Typ.dec_interp t_i t1) _ _ _ (Typ.comp_interp t_i t2) _ v_vale1 v_vale2 v_vale3) (v_vald1')). intro H25. specialize (H25 Htid1'). unfold Atom.interp_form_hatom, interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Heq6. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Heq7, Heq8. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Htic1, Htic2, Htid1, Htid2. subst. intros. simpl. rewrite !Typ.cast_refl. unfold apply_binop. unfold Bval. rewrite !Atom.t_interp_wf in Htib1''; trivial. rewrite Htib1 in Htib1''. inversion Htib1''. rewrite !Atom.t_interp_wf in Htib2''; trivial. rewrite Htib2 in Htib2''. inversion Htib2''. rewrite !Typ.cast_refl. unfold interp_bool. rewrite Typ.cast_refl. apply Typ.i_eqb_spec. rewrite !Atom.t_interp_wf in Htid1''; trivial. rewrite Htid1 in Htid1''. inversion Htid1''. subst. rewrite (Atom.Bval_inj2 _ _ (v_vald1) (store v_vale1 v_vale2 v_vale3) Htid1''). rewrite Htie1 in Htic1. rewrite (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (v_vale1) (v_valc1) Htic1). simpl in isif. rewrite !Typ.cast_refl in isif. apply Typ.i_eqb_spec_false in isif. rewrite !Atom.t_interp_wf in Htic2''; trivial. destruct Heq11d as [((Heq11d1,Heq11d2),Heq11d3) | ((Heq11d1,Heq11d2),Heq11d3) ]; subst; intros; rewrite Htid2 in Htic2; rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite Htie2 in Htia1. rewrite Htia2 in Htic2''. rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia1) in *. rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *. symmetry; now apply read_over_other_write. + rewrite Htie2 in Htia2. rewrite Htia1 in Htic2''. rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia2) in *. rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *. symmetry; apply read_over_other_write; now auto. - unfold store_of_me. case_eq (t_atom .[ c1]); try discriminate. intros [ t5 t6 ] e1 e2 e3 Heq10 [[ti3 te3] i1]. case_eq (e1 =? d1); try discriminate. intros Heq11d. intro HT. injection HT. intros E2 T6 T5 [ ]. subst i1 te3 ti3. clear HT. case_eq ( Typ.eqb t t5 && Typ.eqb v_typeb1' t6 && ((e2 =? a1) && (c2 =? a2) && (d2 =? a2) || (e2 =? a2) && (c2 =? a1) && (d2 =? a1))); simpl; intros Heq11; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. case_eq (Lit.interp rho i). intros isit. easy. intros isif. rewrite orb_false_l. specialize (rho_interp ( Lit.blit i)). rewrite Heq3 in rho_interp. simpl in rho_interp. unfold Lit.interp in isif. rewrite Heq in isif. unfold Var.interp in isif. rewrite rho_interp in isif. unfold Atom.interp_form_hatom, interp_hatom in isif. rewrite Atom.t_interp_wf in isif; trivial. rewrite Heq5 in isif. simpl in isif. unfold interp_bool in isif. unfold Lit.interp. rewrite Heq2. unfold Var.interp. rewrite !wf_interp_form; trivial. rewrite Heq4. simpl. rewrite !andb_true_iff in Heq11. destruct Heq11 as ((Heq11a, Heq11b), Heq11c). rewrite !orb_true_iff in Heq11c. apply Typ.eqb_spec in Heq11a. apply Typ.eqb_spec in Heq11b. apply Int63.eqb_spec in Heq11d. rewrite !andb_true_iff in Heq11c. rewrite !Int63.eqb_spec in Heq11c. rewrite !Atom.t_interp_wf in isif; trivial. rewrite Htia1, Htia2 in isif. simpl in isif. unfold Bval in isif. rewrite !Typ.cast_refl in isif. assert (H25: c1 <? PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq10. discriminate. apply H2 in H25. rewrite Heq10 in H25. simpl in H25. rewrite !andb_true_iff in H25. destruct H25 as (((H25, H29), H28), H27). unfold get_type', v_type in H25, H27, H28, H29. case_eq (t_interp .[ c1]). intros v_typec1' v_valc1' Htic1'. rewrite Htic1' in H25. case_eq v_typec1'; intros; rewrite H10 in H25; try now contradict H25. rewrite andb_true_iff in H25; destruct H25 as (H25a, H25b). case_eq (t_interp .[ e1]). intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H29. case_eq (t_interp .[ e2]). intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H28. case_eq (t_interp .[ e3]). intros v_typee3 v_vale3 Htie3. rewrite Htie3 in H27. pose proof Htic1' as Htic1''. rewrite Atom.t_interp_wf in Htic1', Htie1, Htie2, Htie3; trivial. rewrite Heq10 in Htic1'. simpl in Htic1'. rewrite !Atom.t_interp_wf in Htic1'; trivial. rewrite Htie1, Htie2, Htie3 in Htic1'. simpl in Htic1'. apply Typ.eqb_spec in H25a. apply Typ.eqb_spec in H25b. apply Typ.eqb_spec in H27. apply Typ.eqb_spec in H28. apply Typ.eqb_spec in H29. generalize dependent v_vale1. generalize dependent v_vale2. generalize dependent v_vale3. generalize dependent v_valc1'. rewrite H27, H28, H29. rewrite !Typ.cast_refl. intros. simpl in Htic1'. unfold Bval in Htic1'. generalize dependent v_vale1. generalize dependent v_vale2. generalize dependent v_vale3. generalize dependent v_valc1'. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (@store _ _ (Typ.dec_interp t_i t1) _ _ _ (Typ.comp_interp t_i t2) _ v_vale1 v_vale2 v_vale3) (v_valc1')). intro H25. specialize (H25 Htic1'). unfold Atom.interp_form_hatom, interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Heq6. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Heq7, Heq8. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Htid1, Htic2, Htic1, Htid2. subst. intros. simpl. rewrite !Typ.cast_refl. unfold apply_binop. unfold Bval. rewrite !Atom.t_interp_wf in Htib1''; trivial. rewrite Htib1 in Htib1''. inversion Htib1''. rewrite !Atom.t_interp_wf in Htib2''; trivial. rewrite Htib2 in Htib2''. inversion Htib2''. rewrite !Typ.cast_refl. unfold interp_bool. rewrite Typ.cast_refl. apply Typ.i_eqb_spec. rewrite !Atom.t_interp_wf in Htic1''; trivial. rewrite Htic1 in Htic1''. inversion Htic1''. subst. rewrite (Atom.Bval_inj2 _ _ (v_valc1) (store v_vale1 v_vale2 v_vale3) Htic1''). rewrite Htie1 in Htid1. rewrite (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (v_vale1) (v_vald1) Htid1). apply Typ.i_eqb_spec_false in isif. rewrite !Atom.t_interp_wf in Htic2''; trivial. destruct Heq11c as [((Heq11c1,Heq11c2),Heq11c3) | ((Heq11c1,Heq11c2),Heq11c3) ]; subst; intros; rewrite Htid2 in Htic2; rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite Htie2 in Htia1. rewrite Htia2 in Htic2''. rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia1) in *. rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *. now apply read_over_other_write. + rewrite Htie2 in Htia2. rewrite Htia1 in Htic2''. rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia2) in *. rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *. apply read_over_other_write; now auto. Qed.
imports: Bool List Int63 PArray Psatz ZArith Misc State SMT_terms FArray SMT_classes