From 7ce6bf4f7740de4c69877ec9179520bcaa0d014c Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 18 Feb 2022 17:10:13 +0100 Subject: Removed deprecated features --- src/SMT_terms.v | 68 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 34 insertions(+), 34 deletions(-) (limited to 'src/SMT_terms.v') diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 77dc21f..b19f106 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -108,17 +108,17 @@ Module Form. Definition lt_form i h := match h with | Fatom _ | Ftrue | Ffalse => true - | Fnot2 _ l => Lit.blit l < i + | Fnot2 _ l => Lit.blit l - aforallbi (fun _ l => Lit.blit l < i) args - | Fxor a b | Fiff a b => (Lit.blit a < i) && (Lit.blit b < i) - | Fite a b c => (Lit.blit a < i) && (Lit.blit b < i) && (Lit.blit c < i) - | FbbT _ ls => List.forallb (fun l => Lit.blit l < i) ls + aforallbi (fun _ l => Lit.blit l (Lit.blit a (Lit.blit a List.forallb (fun l => Lit.blit l f1 j = f2 j) -> + (forall j, j f1 j = f2 j) -> lt_form i h -> interp_aux f1 h = interp_aux f2 h. Proof. @@ -161,11 +161,11 @@ Module Form. intros;rewrite default_set;trivial. Qed. - Lemma t_interp_wf : forall i, i < PArray.length t_form -> + Lemma t_interp_wf : forall i, i t_interp.[i] = interp_aux (PArray.get t_interp) (t_form.[i]). Proof. set (P' i t := length t = length t_form -> - forall j, j < i -> + forall j, j t.[j] = interp_aux (PArray.get t) (t_form.[j])). assert (P' (length t_form) t_interp). unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i. @@ -179,7 +179,7 @@ Module Form. intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. rewrite H2;trivial. - assert (j < i). + assert (j [|i|]) by (intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0); auto with zarith. @@ -203,7 +203,7 @@ Module Form. Lemma wf_interp_form_lt : forall t_form, wf t_form -> - forall x, x < PArray.length t_form -> + forall x, x interp_state_var t_form x = interp t_form (t_form.[x]). Proof. unfold interp_state_var;intros. @@ -214,7 +214,7 @@ Module Form. forall t_form, PArray.default t_form = Ftrue -> wf t_form -> forall x, interp_state_var t_form x = interp t_form (t_form.[x]). Proof. - intros t Hd Hwf x;case_eq (x < PArray.length t);intros. + intros t Hd Hwf x;case_eq (x cop_eqb o o' - | Auop o t, Auop o' t' => uop_eqb o o' && (t == t') - | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 == t1') && (t2 == t2') + | Auop o t, Auop o' t' => uop_eqb o o' && (t =? t') + | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 =? t1') && (t2 =? t2') | Anop o t, Anop o' t' => nop_eqb o o' && list_beq Int63.eqb t t' | Atop o t1 t2 t3, Atop o' t1' t2' t3' => - top_eqb o o' && (t1 == t1') && (t2 == t2') && (t3 == t3') - | Aapp a la, Aapp b lb => (a == b) && list_beq Int63.eqb la lb + top_eqb o o' && (t1 =? t1') && (t2 =? t2') && (t3 =? t3') + | Aapp a la, Aapp b lb => (a =? b) && list_beq Int63.eqb la lb | _, _ => false end. @@ -2226,15 +2226,15 @@ Qed. Definition lt_atom i a := match a with | Acop _ => true - | Auop _ h => h < i - | Abop _ h1 h2 => (h1 < i) && (h2 < i) - | Atop _ h1 h2 h3 => (h1 < i) && (h2 < i) && (h3 < i) - | Anop _ ha => List.forallb (fun h => h < i) ha - | Aapp f args => List.forallb (fun h => h < i) args + | Auop _ h => h (h1 (h1 List.forallb (fun h => h List.forallb (fun h => h f1 j = f2 j) -> + forall f1 f2 i, (forall j, j f1 j = f2 j) -> forall a, lt_atom i a -> interp_aux f1 a = interp_aux f2 a. Proof. @@ -2277,12 +2277,12 @@ Qed. intros;rewrite default_set;trivial. Qed. - Lemma t_interp_wf_lt : forall i, i < PArray.length t_atom -> + Lemma t_interp_wf_lt : forall i, i t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]). Proof. assert (Bt := to_Z_bounded (length t_atom)). set (P' i t := length t = length t_atom -> - forall j, j < i -> + forall j, j t.[j] = interp_aux (PArray.get t) (t_atom.[j])). assert (P' (length t_atom) t_interp). unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i. @@ -2296,7 +2296,7 @@ Qed. intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. rewrite H2;trivial. - assert (j < i). + assert (j [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);auto with zarith. @@ -2313,7 +2313,7 @@ Qed. Lemma t_interp_wf : forall i, t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]). Proof. - intros i;case_eq (i< PArray.length t_atom);intros. + intros i;case_eq (i + j exists v : interp_t (v_type Typ.type interp_t (a .[ j])), a .[ j] = Bval (v_type Typ.type interp_t (a .[ j])) v) -> - forall l, List.forallb (fun h0 : int => h0 < h) l = true -> + forall l, List.forallb (fun h0 : int => h0 forall (f0: tval), exists v : interp_t @@ -2356,9 +2356,9 @@ Qed. exists true; auto. Qed. - Lemma check_aux_interp_aux_lt : forall h, h < length t_atom -> + Lemma check_aux_interp_aux_lt : forall h, h forall a, - (forall j, j < h -> + (forall j, j exists v, a.[j] = Bval (v_type _ _ (a.[j])) v) -> exists v, interp_aux (get a) (t_atom.[h]) = Bval (v_type _ _ (interp_aux (get a) (t_atom.[h]))) v. @@ -2485,19 +2485,19 @@ Qed. (k3 (Typ.interp t_i) z)); auto. (* N-ary operators *) - intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl. + intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl. intros acc _; exists (distinct (Typ.i_eqb t_i A) (rev acc)); auto. intro acc; rewrite andb_true_iff; intros [H1 H2]; destruct (IH _ H1) as [va Hva]; rewrite Hva; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ i])) A); simpl; try (exists true; auto); intro k; destruct (IHl (k interp_t va :: acc) H2) as [vb Hvb]; exists vb; auto. (* Application *) intros i l H; apply (check_aux_interp_aux_lt_aux a h IH l H (t_func.[i])). Qed. - Lemma check_aux_interp_hatom_lt : forall h, h < length t_atom -> + Lemma check_aux_interp_hatom_lt : forall h, h exists v, t_interp.[h] = Bval (get_type h) v. Proof. assert (Bt := to_Z_bounded (length t_atom)). set (P' i t := length t = length t_atom -> - forall j, j < i -> + forall j, j exists v, t.[j] = Bval (v_type Typ.type interp_t (t.[j])) v). assert (P' (length t_atom) t_interp). unfold t_interp;apply foldi_ind;unfold P';intros. @@ -2508,7 +2508,7 @@ Qed. rewrite e, PArray.get_set_same. apply check_aux_interp_aux_lt; auto. rewrite H2; auto. - assert (j < i). + assert (j [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);auto with zarith. @@ -2519,7 +2519,7 @@ Qed. Lemma check_aux_interp_hatom : forall h, exists v, t_interp.[h] = Bval (get_type h) v. Proof. - intros i;case_eq (i< PArray.length t_atom);intros. + intros i;case_eq (i