diff options
Diffstat (limited to 'src/euf/Euf.v')
| -rw-r--r-- | src/euf/Euf.v | 146 |
1 files changed, 73 insertions, 73 deletions
diff --git a/src/euf/Euf.v b/src/euf/Euf.v index 83220c2..6b97f94 100644 --- a/src/euf/Euf.v +++ b/src/euf/Euf.v @@ -180,7 +180,7 @@ Section certif. apply C.interp_true. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. Qed. - Hint Resolve valid_C_true. + Hint Resolve valid_C_true : smtcoq_euf. Local Notation interp := (Atom.interp t_i t_func t_atom). @@ -210,11 +210,11 @@ Section certif. C.interp rho (get_eq (Lit.blit l) f). Proof. intros l f Hf;unfold get_eq. - case_eq (t_form.[Lit.blit l]);trivial;intros. - case_eq (t_atom.[i]);trivial;intros. - destruct b;trivial. + case_eq (t_form.[Lit.blit l]);trivial with smtcoq_euf;intros. + case_eq (t_atom.[i]);trivial with smtcoq_euf;intros. + destruct b;trivial with smtcoq_euf. generalize wt_t_atom;unfold Atom.wt;unfold is_true; - rewrite PArray.forallbi_spec;intros. + rewrite Misc.aforallbi_spec;intros. assert (i < length t_atom). apply PArray.get_not_default_lt. rewrite H0, def_t_atom;discriminate. @@ -279,48 +279,48 @@ Section certif. C.interp rho (check_trans_aux t1 t2 eqs res c). Proof. induction eqs;simpl;intros. - apply get_eq_interp;intros. + - apply get_eq_interp;intros. match goal with |- context [if ?b then _ else _] => case_eq b end; - intros;trivial. + intros;trivial with smtcoq_euf. simpl;rewrite Lit.interp_lit;unfold Var.interp. - destruct H1;[ | rewrite H1,orb_true_r;auto]. + destruct H1;[ | rewrite H1,orb_true_r;auto with smtcoq_euf smtcoq_core]. rewrite orb_true_iff, !andb_true_iff in H7;destruct H7 as [[H7 H8] | [H7 H8]]. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. - tunicity. subst t. rewrite H4, H1;auto. + tunicity. subst t. rewrite H4, H1;auto with smtcoq_euf smtcoq_core. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. - tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto. - apply get_eq_interp;intros. - destruct (Int63Properties.reflect_eqb t2 b);subst;tunicity; try subst t. - apply (IHeqs u);trivial. + tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto with smtcoq_euf smtcoq_core. + - apply get_eq_interp;intros. + destruct (Misc.reflect_eqb t2 b);subst;tunicity; try subst t. + + apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. rewrite interp_binop_eqb_sym;trivial. - destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity; try subst t. - apply (IHeqs u);trivial. + + destruct (Misc.reflect_eqb t2 a0); subst;tunicity; try subst t. + * apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. - destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity; try subst t. - apply (IHeqs u);trivial. + * destruct (Misc.reflect_eqb t1 b);subst;tunicity; try subst t. + -- apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. - destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto]. + -- destruct (Misc.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto with smtcoq_euf smtcoq_core]. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. @@ -332,9 +332,9 @@ Section certif. C.interp rho (check_trans res eqs). Proof. unfold check_trans;intros res [ | leq eqs]. - apply get_eq_interp;intros. - destruct (Int63Properties.reflect_eqb a b). - unfold C.interp; simpl; rewrite orb_false_r. + - apply get_eq_interp;intros. + destruct (Misc.reflect_eqb a b). + + unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; simpl; rewrite Lit.is_pos_lit. unfold Var.interp; simpl; rewrite Lit.blit_lit. rewrite H1. @@ -344,12 +344,12 @@ Section certif. unfold Atom.interp_hatom. rewrite HHb;simpl;rewrite Typ.cast_refl;simpl. apply Typ.i_eqb_refl. - auto. - apply get_eq_interp;intros. + + auto with smtcoq_euf. + - apply get_eq_interp;intros. apply check_trans_aux_correct with t;trivial. simpl;rewrite Lit.interp_nlit;unfold Var.interp. rewrite <- H1. (* Attention ici on utilise la decidabilit'e de l'egalit'e sur t *) - destruct (rho (Lit.blit leq));auto. + destruct (rho (Lit.blit leq));auto with smtcoq_core. Qed. Inductive Forall2 A B (P:A->B->Prop) : list A -> list B -> Prop := @@ -362,16 +362,16 @@ Section certif. (Forall2 _ _ (fun a b => interp_hatom a = interp_hatom b) l r -> C.interp rho c) -> C.interp rho (build_congr lp l r c). Proof. - induction lp;destruct l;destruct r;simpl;trivial;intros. + induction lp;destruct l;destruct r;simpl;trivial with smtcoq_euf smtcoq_core;intros. apply H;constructor. destruct a. apply get_eq_interp;intros. match goal with |- context [if ?x then _ else _] => - case_eq x;intros;auto end. + case_eq x;intros;auto with smtcoq_euf smtcoq_core end. apply IHlp;simpl;intros. rewrite Lit.interp_nlit;unfold Var.interp. - case_eq (rho (Lit.blit i1));intros;simpl;[ | auto]. - apply H;constructor;trivial. + case_eq (rho (Lit.blit i1));intros;simpl;[ | auto with smtcoq_euf smtcoq_core]. + apply H;constructor;trivial with smtcoq_euf smtcoq_core. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. rewrite Typ.eqb_spec in H4. unfold Atom.get_type in H3, H4. rewrite H3,H4. intros [va HHa] [vb HHb]. revert H7;rewrite H2;unfold Atom.apply_binop; simpl. unfold Atom.interp_hatom. @@ -381,11 +381,11 @@ Section certif. rewrite orb_true_iff, !andb_true_iff in H5;destruct H5 as [ [H5 H7] | [H5 H7]]. rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst. - rewrite HHa, HHb;trivial. + rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core. rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst. - rewrite HHa, HHb;trivial. - destruct (Int63Properties.reflect_eqb i i0);[subst | auto]. - apply IHlp;intros;apply H;constructor;auto. + rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core. + destruct (Misc.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core]. + apply IHlp;intros;apply H;constructor;auto with smtcoq_euf smtcoq_core. Qed. Lemma valid_check_congr : @@ -393,71 +393,71 @@ Section certif. C.interp rho (check_congr leq eqs). Proof. unfold check_congr;intros leq eqs;apply get_eq_interp;intros. - case_eq (t_atom .[ a]);intros;auto; - case_eq (t_atom .[ b]);intros;auto. + case_eq (t_atom .[ a]);intros;auto with smtcoq_euf smtcoq_core; + case_eq (t_atom .[ b]);intros;auto with smtcoq_euf smtcoq_core. (* uop *) - destruct (Atom.reflect_uop_eqb u u0);[subst | auto]. + destruct (Atom.reflect_uop_eqb u u0);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl. rewrite HHb, HHa. simpl. - rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa. - rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb. + rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. + rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). inversion H6;subst. unfold Atom.interp_hatom in H10. - rewrite <- HHa; rewrite <- HHb, H10;trivial. + rewrite <- HHa; rewrite <- HHb, H10;trivial with smtcoq_euf smtcoq_core. inversion H7. - apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial. + apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. - intros x y;destruct (Typ.reflect_eqb x y);auto. + intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. (* bop *) - destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto]. + destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop. unfold Atom.interp_hatom;simpl. rewrite HHb, HHa;simpl. - rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa. - rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb. + rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. + rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). inversion H6;clear H6;subst. inversion H12;clear H12;subst. unfold Atom.interp_hatom in H10, H8. - rewrite <- HHa. rewrite <- HHb, H10, H8;trivial. + rewrite <- HHa. rewrite <- HHb, H10, H8;trivial with smtcoq_euf smtcoq_core. inversion H7. - apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial. + apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. - intros x y;destruct (Typ.reflect_eqb x y);auto. + intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. (* op *) - destruct (Int63Properties.reflect_eqb i i0);[subst | auto]. + destruct (Misc.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl. rewrite HHb, HHa;simpl. - rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa. - rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb. + rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. + rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). rewrite <- HHa;rewrite <- HHb;destruct (t_func.[i0]). apply f_equal;clear HHa HHb va vb H5 H4. - induction H6;simpl;trivial. + induction H6;simpl;trivial with smtcoq_euf smtcoq_core. unfold Atom.interp_hatom in H4. - rewrite IHForall2, H4;trivial. + rewrite IHForall2, H4;trivial with smtcoq_euf smtcoq_core. inversion H7. - apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial. + apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. - intros x y;destruct (Typ.reflect_eqb x y);auto. + intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. Qed. Lemma valid_check_congr_pred : @@ -465,18 +465,18 @@ Section certif. C.interp rho (check_congr_pred lpa lpb eqs). Proof. unfold check_congr_pred;intros. - case_eq (t_form.[Lit.blit lpa]);auto. - case_eq (t_form.[Lit.blit lpb]);auto;intros. - case_eq (t_atom.[i0]);auto; case_eq (t_atom.[i]);auto;intros. + case_eq (t_form.[Lit.blit lpa]);auto with smtcoq_euf smtcoq_core. + case_eq (t_form.[Lit.blit lpb]);auto with smtcoq_euf smtcoq_core;intros. + case_eq (t_atom.[i0]);auto with smtcoq_euf smtcoq_core; case_eq (t_atom.[i]);auto with smtcoq_euf smtcoq_core;intros. (* uop *) - destruct (Atom.reflect_uop_eqb u0 u);[subst | auto]. + destruct (Atom.reflect_uop_eqb u0 u);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). destruct (rho (Lit.blit lpa));reflexivity. rewrite !wf_interp_form, H, H0;simpl. generalize wt_t_atom;unfold Atom.wt;unfold is_true; - rewrite PArray.forallbi_spec;intros. + rewrite Misc.aforallbi_spec;intros. assert (i < length t_atom). apply PArray.get_not_default_lt. rewrite H1, def_t_atom;discriminate. @@ -485,19 +485,19 @@ Section certif. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. - rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial. + rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. apply f_equal;apply f_equal. - inversion H3;clear H3;subst;trivial. + inversion H3;clear H3;subst;trivial with smtcoq_euf smtcoq_core. (* bop *) - destruct (Atom.reflect_bop_eqb b0 b);[subst | auto]. + destruct (Atom.reflect_bop_eqb b0 b);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). destruct (rho (Lit.blit lpa));reflexivity. rewrite !wf_interp_form, H, H0;simpl. generalize wt_t_atom;unfold Atom.wt;unfold is_true; - rewrite PArray.forallbi_spec;intros. + rewrite Misc.aforallbi_spec;intros. assert (i < length t_atom). apply PArray.get_not_default_lt. rewrite H1, def_t_atom. discriminate. @@ -506,20 +506,20 @@ Section certif. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. - rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial. + rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. inversion H3;clear H3;subst. inversion H11;clear H11;subst. - apply f_equal; apply f_equal2;trivial. + apply f_equal; apply f_equal2;trivial with smtcoq_euf smtcoq_core. (* op *) - destruct (Int63Properties.reflect_eqb i2 i1);[subst | auto]. + destruct (Misc.reflect_eqb i2 i1);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). destruct (rho (Lit.blit lpa));reflexivity. rewrite !wf_interp_form, H, H0;simpl. generalize wt_t_atom;unfold Atom.wt;unfold is_true; - rewrite PArray.forallbi_spec;intros. + rewrite Misc.aforallbi_spec;intros. assert (i < length t_atom). apply PArray.get_not_default_lt. rewrite H1, def_t_atom;discriminate. @@ -528,11 +528,11 @@ Section certif. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. - rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial. + rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. apply f_equal;destruct (t_func.[i1]);apply f_equal. clear H H0 H1 H2 H5 H6. - induction H3;simpl;trivial. - unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial. + induction H3;simpl;trivial with smtcoq_euf smtcoq_core. + unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial with smtcoq_euf smtcoq_core. Qed. End Proof. |