Remove dependency on proof irrelevence axiom

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.

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.

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.
 

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:?.

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

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,13 +54,24 @@ 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
   | _, None => True
   | 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.
 

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

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.

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].