diff --git a/arm/Op.v b/arm/Op.v index 60c214d082..b3d228ad4e 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -24,6 +24,7 @@ syntax and dynamic semantics of the Cminor language. *) +Require Import Eqdep_dec. Require Import Axioms. Require Import Coqlib. Require Import AST. @@ -159,7 +160,7 @@ Proof. generalize Int.eq_dec; intro. assert (forall (x y: shift_amount), {x=y}+{x<>y}). destruct x as [x Px]. destruct y as [y Py]. destruct (H x y). - subst x. rewrite (proof_irr Px Py). left; auto. + subst x. replace Px with Py. left; auto. apply UIP_dec. decide equality. right. red; intro. elim n. inversion H0. auto. decide equality. Defined. diff --git a/backend/Debugvar.v b/backend/Debugvar.v index 1f36103017..0902c68703 100644 --- a/backend/Debugvar.v +++ b/backend/Debugvar.v @@ -27,6 +27,14 @@ Fixpoint safe_builtin_arg {A: Type} (a: builtin_arg A) : Prop := | _ => False end. +Lemma safe_builtin_arg_irr {A} (a: builtin_arg A) (p0 p1 : safe_builtin_arg a): p0 = p1. +Proof. + induction a; try solve [destruct p0; destruct p1; reflexivity]. + destruct p0 as [p0h p0l]. + destruct p1 as [p1h p1l]. + f_equal; auto. +Qed. + Definition debuginfo := { a : builtin_arg loc | safe_builtin_arg a }. (** Normalization of debug info. Prefer an actual location to a constant. @@ -144,7 +152,7 @@ Global Opaque eq_arg. Definition eq_debuginfo (i1 i2: debuginfo) : {i1=i2} + {i1 <> i2}. Proof. destruct (eq_arg (proj1_sig i1) (proj1_sig i2)). - left. destruct i1, i2; simpl in *. subst x0. f_equal. apply proof_irr. + left. destruct i1, i2; simpl in *. subst x0. f_equal. apply safe_builtin_arg_irr. right. congruence. Defined. Global Opaque eq_debuginfo. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 036b768bca..1cc170cd34 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -15,6 +15,7 @@ (** Type expressions for the Compcert C and Clight languages *) +Require Import Eqdep_dec. Require Import Axioms Coqlib Maps Errors. Require Import AST Linking. Require Archi. @@ -1256,9 +1257,20 @@ Lemma composite_eq: Build_composite su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 = Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2. Proof. intros. subst. - assert (pos1 = pos2) by apply proof_irr. - assert (al2p1 = al2p2) by apply proof_irr. - assert (szal1 = szal2) by apply proof_irr. + assert (pos1 = pos2). + apply functional_extensionality. intros x. destruct (pos1 x). + assert (al2p1 = al2p2). + clear. destruct al2p1 as [n1 Hn1]. destruct al2p2 as [n2 Hn2]. + generalize Hn2. replace n2 with n1. intros Hn2'. f_equal. apply UIP_dec. apply Z.eq_dec. + rewrite Hn1 in Hn2. rewrite !two_power_nat_equiv in Hn2. apply Nat2Z.inj. + refine (Z.pow_inj_r _ _ _ _ _ _ Hn2); auto with zarith. + assert (szal1 = szal2). + clear -al2p2. destruct szal1 as [n1 Hn1]. destruct szal2 as [n2 Hn2]. + generalize Hn2. replace n2 with n1. intros Hn2'. f_equal. apply UIP_dec. apply Z.eq_dec. + rewrite Hn1 in Hn2. eapply Z.mul_reg_r;[|apply Hn2]. + destruct al2p2 as [n ->]. + assert (Hn := two_power_nat_pos n). + omega. subst. reflexivity. Qed. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index d37fbd4637..317bcc7f55 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -1199,7 +1199,7 @@ Proof. intros. assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. } exploit Mem.perm_drop_2; eauto. intros ORD. - split. omega. inv ORD; auto. + split. omega. destruct p; elim ORD; reflexivity. * set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. diff --git a/common/Memdata.v b/common/Memdata.v index a9ed48b445..bfbac578de 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -157,6 +157,17 @@ Inductive memval: Type := | Byte: byte -> memval | Fragment: val -> quantity -> nat -> memval. +Lemma memval_dec (a b: memval): {a = b} + {a <> b}. +Proof. + repeat decide equality; + solve [apply Byte.eq_dec + |apply Int.eq_dec + |apply Int64.eq_dec + |apply Float.eq_dec + |apply Float32.eq_dec + |apply Ptrofs.eq_dec]. +Qed. + (** * Encoding and decoding integers *) (** We define functions to convert between integers and lists of bytes diff --git a/common/Memory.v b/common/Memory.v index 2cf1c3ab3b..7773b43797 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -26,6 +26,7 @@ - [free]: invalidate a memory block. *) +Require Import Eqdep_dec. Require Import Zwf. Require Import Axioms. Require Import Coqlib. @@ -53,6 +54,11 @@ Definition perm_order' (po: option permission) (p: permission) := | None => False end. +Lemma perm_order'_irr p1 p2 (po1 po2: perm_order' p1 p2): po1 = po2. +Proof. + destruct p1 as [p1|];[apply perm_order_irr|elim po1]. +Qed. + Definition perm_order'' (po1 po2: option permission) := match po1, po2 with | Some p1, Some p2 => perm_order p1 p2 @@ -60,6 +66,12 @@ Definition perm_order'' (po1 po2: option permission) := | None, Some _ => False end. +Lemma perm_order''_irr p1 p2 (po1 po2: perm_order'' p1 p2): po1 = po2. +Proof. + destruct p1 as [p1|];destruct p2 as [p2|]; try apply perm_order_irr; + destruct po1; destruct po2; reflexivity. +Qed. + Record mem' : Type := mkmem { mem_contents: PMap.t (ZMap.t memval); (**r [block -> offset -> memval] *) mem_access: PMap.t (Z -> perm_kind -> option permission); @@ -80,7 +92,10 @@ Lemma mkmem_ext: cont1=cont2 -> acc1=acc2 -> next1=next2 -> mkmem cont1 acc1 next1 a1 b1 c1 = mkmem cont2 acc2 next2 a2 b2 c2. Proof. - intros. subst. f_equal; apply proof_irr. + intros. subst. f_equal; repeat (apply functional_extensionality_dep; intro). + - apply perm_order''_irr. + - apply UIP_dec. repeat decide equality. + - apply UIP_dec. apply memval_dec. Qed. (** * Validity of blocks and accesses *) @@ -2129,7 +2144,7 @@ Proof. intros. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool. - rewrite zle_true. rewrite zlt_true. simpl. constructor. + rewrite zle_true. rewrite zlt_true. simpl. auto with mem. omega. omega. Qed. diff --git a/common/Memtype.v b/common/Memtype.v index ae4fa5fdbf..dc220e6c40 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -23,6 +23,7 @@ - [free]: invalidate a memory block. *) +Require Import Eqdep_dec. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -54,18 +55,49 @@ Inductive permission: Type := (** In the list, each permission implies the other permissions further down the list. We reflect this fact by the following order over permissions. *) -Inductive perm_order: permission -> permission -> Prop := - | perm_refl: forall p, perm_order p p - | perm_F_any: forall p, perm_order Freeable p - | perm_W_R: perm_order Writable Readable - | perm_any_N: forall p, perm_order p Nonempty. +Definition perm_order (p1 p2: permission): Prop := + match p1, p2 with + | Freeable, _ => True + | Writable, Readable => True + | _, Nonempty => True + | x, y => x = y + end. + +Lemma perm_refl: forall p, perm_order p p. +Proof. + destruct p; constructor. +Qed. +Hint Resolve perm_refl: mem. -Hint Constructors perm_order: mem. +Lemma perm_F_any: forall p, perm_order Freeable p. +Proof. + constructor. +Qed. +Hint Resolve perm_F_any: mem. + +Lemma perm_W_R: perm_order Writable Readable. +Proof. + constructor. +Qed. +Hint Resolve perm_W_R: mem. + +Lemma perm_any_N: forall p, perm_order p Nonempty. +Proof. + destruct p; constructor. +Qed. +Hint Resolve perm_any_N: mem. + +Lemma perm_order_irr : forall p1 p2 (po1 po2: perm_order p1 p2), po1 = po2. +Proof. + destruct p1; destruct p2; try discriminate; cbn; + destruct po1; try destruct po2; try reflexivity; + apply UIP_dec; decide equality. +Qed. Lemma perm_order_trans: forall p1 p2 p3, perm_order p1 p2 -> perm_order p2 p3 -> perm_order p1 p3. Proof. - intros. inv H; inv H0; constructor. + destruct p1; destruct p2; destruct p3; try constructor; discriminate. Qed. (** Each address has not one, but two permissions associated diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index 2e64b8da09..76e40cb501 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -14,7 +14,7 @@ (* *********************************************************************) Require Import Streams. -Require Import ProofIrrelevance. +Require Import Eqdep. Require Import Equality. Require Import List. Require Import Syntax. @@ -445,7 +445,7 @@ destruct (compare_eqdec (last_symb_of_non_init_state state) head_symbolt); intui eapply JMeq_sym, JMeq_trans, JMeq_sym, JMeq_eq in H1; [|apply JMeq_eqrect with (e:=e)]. rewrite <- H1. simpl in pop_ptlz_pop_stack_compat. -erewrite proof_irrelevance with (p1:=pop_ptlz_pop_stack_compat_converter _ _ _ _ _). +erewrite UIP with (p1:=pop_ptlz_pop_stack_compat_converter _ _ _ _ _). apply pop_ptlz_pop_stack_compat. Transparent AlphabetComparable AlphabetComparableUsualEq. Qed. diff --git a/lib/Axioms.v b/lib/Axioms.v index fdc89920d6..85667f3b83 100644 --- a/lib/Axioms.v +++ b/lib/Axioms.v @@ -41,11 +41,3 @@ Proof @FunctionalExtensionality.functional_extensionality. Lemma extensionality: forall {A B: Type} (f g : A -> B), (forall x, f x = g x) -> f = g. Proof @functional_extensionality. - -(** * Proof irrelevance *) - -(** We also use proof irrelevance. *) - -Axiom proof_irr: ClassicalFacts.proof_irrelevance. - -Arguments proof_irr [A].