proposition: Lemma prop_check_eq: forall bs1 bs2 bsres, (length bs1) = (length bs2) -> check_eq bs1 bs2 bsres = true -> forallb2 Bool.eqb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) = forallb (Lit.interp rho) bsres.
proof: Proof. intro bs1. induction bs1 as [ | x1 bs1 IHbs1 ]. - intros bs2 bsres Hlen Hcheck. case bs2 in *. + case bsres in *. * now simpl. * contradict Hcheck; now simpl. + contradict Hcheck; now simpl. - intros bs2 bsres Hlen Hcheck. symmetry. case bs2 in *. + case bsres in *; contradict Hcheck; now simpl. + case bsres in *. * contradict Hcheck; now simpl. * simpl. rename i into x2. rename i0 into r1. simpl in Hlen. inversion Hlen. rename H0 into Hlen'. case bsres in *. simpl in Hcheck. case_eq (Lit.is_pos r1); intros; rewrite H in Hcheck; try (case bs1 in *; try (now contradict Hcheck); case bs2 in *; try (now contradict Hcheck)); rename H into Hposr1; case_eq (t_form .[ Lit.blit r1]);intros; rewrite H in Hcheck; try (now contradict Hcheck); rename H into Hform_r1; generalize (rho_interp (Lit.blit r1)); rewrite Hform_r1; simpl; intro Hi. rename i into arg1; rename i0 into arg2. unfold Lit.interp at 1, Var.interp at 1. rewrite Hposr1, Hi. repeat (rewrite andb_true_r). case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)). intros Hif. rewrite orb_true_iff in Hif. repeat (rewrite andb_true_iff in Hif). repeat (rewrite eqb_spec in Hif). destruct Hif as [ Hif1 | Hif2 ]. destruct Hif1 as (Hx1, Hx2). now rewrite Hx1, Hx2. destruct Hif2 as (Hx2, Hx1). rewrite Hx1, Hx2. now rewrite bool_eqb_comm. intros Hif. rewrite Hif in Hcheck. now contradict Hcheck. case_eq (to_list a); intros; rewrite H in Hcheck; try (now contradict Hcheck). rename H into Ha, i1 into a1, l into rargs. case_eq (Lit.is_pos a1); intros; rewrite H in Hcheck; try (now contradict Hcheck). rename H into Hposa1. case_eq (t_form .[ Lit.blit a1]); intros; rewrite H in Hcheck; try (now contradict Hcheck). rename H into Hform_a1. rename i into x1', i0 into x2', i1 into arg1, i2 into arg2. generalize (rho_interp (Lit.blit a1)). rewrite Hform_a1. simpl. intro Heqx1x2. rewrite afold_left_and in Hi. rewrite Ha in Hi. simpl in Hi. unfold Lit.interp at 1, Var.interp at 1. rewrite Hposr1, Hi. repeat (rewrite andb_true_r). unfold Lit.interp at 1, Var.interp at 1. rewrite Hposa1. rewrite Heqx1x2. case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)). intros Hif. rewrite Hif in Hcheck. apply (@IHbs1 _ _ Hlen') in Hcheck. simpl in Hcheck. rewrite Hcheck. repeat (rewrite orb_true_iff in Hif). repeat (rewrite andb_true_iff in Hif). repeat (rewrite eqb_spec in Hif). destruct Hif as [ Hif1 | Hif2 ]. destruct Hif1 as (Hx1, Hx2). now rewrite Hx1, Hx2. destruct Hif2 as (Hx2, Hx1). rewrite Hx1, Hx2. now rewrite bool_eqb_comm. intros Hif. rewrite Hif in Hcheck. now contradict Hcheck. simpl in Hcheck. case_eq (Lit.is_pos r1); intros; rewrite H in Hcheck; try (case bs1 in *; try (now contradict Hcheck); case bs2 in *; try (now contradict Hcheck)); rename H into Hposr1; case_eq (t_form .[ Lit.blit r1]);intros; rewrite H in Hcheck; try (now contradict Hcheck); rename H into Hform_r1; generalize (rho_interp (Lit.blit r1)); rewrite Hform_r1; simpl; intro Hi. contradict Hcheck. simpl. case ((i0 =? x1) && (i1 =? x2) || (i0 =? x2) && (i1 =? x1)); easy. rename i0 into x1', i1 into x2', i2 into arg1, i3 into arg2. unfold Lit.interp at 1, Var.interp at 1. rewrite Hposr1, Hi. case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)). intros Hif. rewrite Hif in Hcheck. apply (@IHbs1 _ _ Hlen') in Hcheck. simpl in Hcheck. rewrite Hcheck. repeat (rewrite orb_true_iff in Hif). repeat (rewrite andb_true_iff in Hif). repeat (rewrite eqb_spec in Hif). destruct Hif as [ Hif1 | Hif2 ]. destruct Hif1 as (Hx1, Hx2). now rewrite Hx1, Hx2. destruct Hif2 as (Hx2, Hx1). rewrite Hx1, Hx2. now rewrite bool_eqb_comm. intros Hif. rewrite Hif in Hcheck. now contradict Hcheck. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance