proposition: Lemma valid_check_diseq : forall c, C.valid rho (check_diseq c).
proof: Proof. unfold check_diseq; intro c. case_eq (t_form.[Lit.blit c]);intros;subst; try (unfold C.valid; apply valid_C_true; trivial). case_eq ((length a) =? 3); intros; try (unfold C.valid; apply valid_C_true; trivial). apply eqb_correct in H0. apply get_eq_interp; intros. apply get_not_le_interp; intros. apply get_not_le_interp; intros. case_eq ((a0 =? a1) && (a0 =? b1) && (b =? b0) && (b =? a2)); intros; subst; try (unfold C.valid; apply valid_C_true; trivial). repeat(apply andb_prop in H19; destruct H19). apply Int63.eqb_spec in H19;apply Int63.eqb_spec in H20;apply Int63.eqb_spec in H21;apply Int63.eqb_spec in H22; subst a0 b. unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; rewrite Lit.is_pos_lit. unfold Var.interp; rewrite Lit.blit_lit. rewrite wf_interp_form, H;simpl. case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])). intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19. apply (afold_left_orb_true 0); rewrite ?length_amap, ?get_amap; [ rewrite H0; reflexivity | assumption | rewrite H0; reflexivity ]. apply (afold_left_orb_true 1); rewrite ?length_amap, ?get_amap; [ rewrite H0; reflexivity | assumption | rewrite H0; reflexivity ]. apply (afold_left_orb_true 2); rewrite ?length_amap, ?get_amap; [ rewrite H0; reflexivity | assumption | rewrite H0; reflexivity ]. intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19. unfold Lit.interp in H19. rewrite H3 in H19; unfold Var.interp in H19; rewrite H4 in H19. unfold Lit.interp in H21. pose (H24 := H15). apply negb_true_iff in H24. rewrite H24 in H21. unfold Var.interp in H21; rewrite H16 in H21. unfold Lit.interp in H23. pose (H25 := H9). apply negb_true_iff in H25. rewrite H25 in H23. unfold Var.interp in H23; rewrite H10 in H23. assert (t = Typ.TZ). generalize H12. clear H12. destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) Typ.TZ) as [H12|H12]; [intros _|discriminate]. generalize H6. clear H6. destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) t) as [H6|H6]; [intros _|discriminate]. rewrite <- H6. auto with smtcoq_core. rewrite H26 in H19. case_eq (interp_atom (t_atom .[ b1])); intros t1 v1 Heq1. assert (H50: t1 = Typ.TZ). unfold get_type, get_type' in H18. rewrite t_interp_wf in H18; trivial. rewrite Heq1 in H18. simpl in H18. rewrite Typ.eqb_spec in H18. assumption. subst t1. case_eq (interp_atom (t_atom .[ a2])); intros t2 v2 Heq2. assert (H50: t2 = Typ.TZ). unfold get_type, get_type' in H17. rewrite t_interp_wf in H17; trivial. rewrite Heq2 in H17. simpl in H17. rewrite Typ.eqb_spec in H17. assumption. subst t2. subst;elim (interp_binop_eqb_antisym (t_atom.[b1]) (t_atom.[a2]) v1 v2);trivial. unfold interp_hatom in H19; do 2 rewrite t_interp_wf in H19; trivial. unfold interp_hatom in H23; do 2 rewrite t_interp_wf in H23; trivial. unfold interp_hatom in H21; do 2 rewrite t_interp_wf in H21; trivial. trivial. destruct H19. case_eq ((a0 =? b0) && (a0 =? a2) && (b =? a1) && (b =? b1)); intros; subst; try (unfold C.valid; apply valid_C_true; trivial). repeat(apply andb_prop in H19; destruct H19). apply Int63.eqb_spec in H19;apply Int63.eqb_spec in H20;apply Int63.eqb_spec in H21;apply Int63.eqb_spec in H22;subst a0 b. unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; rewrite Lit.is_pos_lit. unfold Var.interp; rewrite Lit.blit_lit. rewrite wf_interp_form, H;simpl. case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])). intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19. apply (afold_left_orb_true 0); rewrite ?length_amap, ?get_amap; [ rewrite H0; reflexivity | assumption | rewrite H0; reflexivity ]. apply (afold_left_orb_true 1); rewrite ?length_amap, ?get_amap; [ rewrite H0; reflexivity | assumption | rewrite H0; reflexivity ]. apply (afold_left_orb_true 2); rewrite ?length_amap, ?get_amap; [ rewrite H0; reflexivity | assumption | rewrite H0; reflexivity ]. intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19. unfold Lit.interp in H19. rewrite H3 in H19; unfold Var.interp in H19; rewrite H4 in H19. unfold Lit.interp in H21. case_eq (Lit.is_pos (a.[2])); intros. apply negb_true_iff in H15;rewrite H15 in H24; discriminate. rewrite H24 in H21. unfold Var.interp in H21;rewrite H16 in H21. unfold Lit.interp in H23. case_eq (Lit.is_pos (a.[1])); intros. apply negb_true_iff in H9; rewrite H9 in H25; discriminate. rewrite H25 in H23. unfold Var.interp in H23; rewrite H10 in H23. rewrite <-H22, <- H20 in H21. assert (t = Typ.TZ). rewrite Typ.eqb_spec in H6; rewrite Typ.eqb_spec in H18; subst; auto with smtcoq_core. rewrite H26 in H19. case_eq (interp_atom (t_atom .[ b0])); intros t1 v1 Heq1. assert (H50: t1 = Typ.TZ). unfold get_type, get_type' in H12. rewrite t_interp_wf in H12; trivial. rewrite Heq1 in H12. simpl in H12. rewrite Typ.eqb_spec in H12. assumption. subst t1. case_eq (interp_atom (t_atom .[ a1])); intros t2 v2 Heq2. assert (H50: t2 = Typ.TZ). unfold get_type, get_type' in H11. rewrite t_interp_wf in H11; trivial. rewrite Heq2 in H11. simpl in H11. rewrite Typ.eqb_spec in H11. assumption. subst t2. elim (interp_binop_eqb_antisym (t_atom.[b0]) (t_atom.[a1]) v1 v2); trivial. unfold interp_hatom in H19; do 2 rewrite t_interp_wf in H19; trivial. unfold interp_hatom in H21; do 2 rewrite t_interp_wf in H21; trivial. unfold interp_hatom in H23; do 2 rewrite t_interp_wf in H23; trivial. trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz