Commit 4ef67160 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added equality on radix.

parent 6ff8453d
...@@ -980,10 +980,46 @@ Qed. ...@@ -980,10 +980,46 @@ Qed.
End Even_Odd. End Even_Odd.
Section Proof_Irrelevance.
Scheme eq_dep_elim := Induction for eq Sort Type.
Definition eqbool_dep P (h1 : P true) b :=
match b return P b -> Prop with
| true => fun (h2 : P true) => h1 = h2
| false => fun (h2 : P false) => False
end.
Lemma eqbool_irrelevance : forall (b : bool) (h1 h2 : b = true), h1 = h2.
Proof.
assert (forall (h : true = true), refl_equal true = h).
apply (eq_dep_elim bool true (eqbool_dep _ _) (refl_equal _)).
intros b.
case b.
intros h1 h2.
now rewrite <- (H h1).
intros h.
discriminate h.
Qed.
End Proof_Irrelevance.
Section pow. Section pow.
Record radix := { radix_val : Z ; radix_prop : Zle_bool 2 radix_val = true }. Record radix := { radix_val : Z ; radix_prop : Zle_bool 2 radix_val = true }.
Theorem radix_val_inj :
forall r1 r2, radix_val r1 = radix_val r2 -> r1 = r2.
Proof.
intros (r1, H1) (r2, H2) H.
simpl in H.
revert H1.
rewrite H.
intros H1.
apply f_equal.
apply eqbool_irrelevance.
Qed.
Variable r : radix. Variable r : radix.
Theorem radix_gt_1 : (1 < radix_val r)%Z. Theorem radix_gt_1 : (1 < radix_val r)%Z.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment