feat(library/init/logic): add 'arbitrary'

It is identical to default, but it is opaque.
That is, when we use 'arbitrary A', we cannot rely on the particular
value selected.

library/init/logic.lean

@@ -332,6 +332,9 @@ inhabited.rec H2 H1
 definition inhabited.default (A : Type) [H : inhabited A] : A :=
 inhabited.rec (λa, a) H
 
+opaque definition arbitrary (A : Type) [H : inhabited A] : A :=
+inhabited.rec (λa, a) H
+
 definition Prop_inhabited [instance] : inhabited Prop :=
 inhabited.mk true
 

tests/lean/run/eq12.lean

@@ -4,7 +4,7 @@ definition diag : bool → bool → bool → nat,
 diag _  tt ff := 1,
 diag ff _  tt := 2,
 diag tt ff _  := 3,
-diag _  _  _  := default nat
+diag _  _  _  := arbitrary nat
 
 theorem diag1 (a : bool) : diag a tt ff = 1 :=
 bool.cases_on a rfl rfl
@@ -15,8 +15,8 @@ bool.cases_on a rfl rfl
 theorem diag3 (a : bool) : diag tt ff a = 3 :=
 bool.cases_on a rfl rfl
 
-theorem diag4_1 : diag ff ff ff = default nat :=
+theorem diag4_1 : diag ff ff ff = arbitrary nat :=
 rfl
 
-theorem diag4_2 : diag tt tt tt = default nat :=
+theorem diag4_2 : diag tt tt tt = arbitrary nat :=
 rfl

tests/lean/run/eq13.lean

@@ -1,9 +1,9 @@
-open nat inhabited
+open nat
 
 definition f : nat → nat → nat,
 f _ 0 := 0,
 f 0 _ := 1,
-f _ _ := 2
+f _ _ := arbitrary nat
 
 theorem f_zero_right : ∀ a, f a 0 = 0,
 f_zero_right 0        := rfl,
@@ -12,5 +12,5 @@ f_zero_right (succ _) := rfl
 theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
 rfl
 
-theorem f_succ_succ (a b : nat) : f (a+1) (b+1) = 2 :=
+theorem f_succ_succ (a b : nat) : f (a+1) (b+1) = arbitrary nat :=
 rfl