From da719e6ee407c8fc0ca7aee1d811a072eb835506 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 15 Dec 2014 16:13:04 -0500 Subject: [PATCH] refactor(library/logic): rename theorems --- library/logic/axioms/hilbert.lean | 6 +-- library/logic/cast.lean | 37 +++++++++------- library/logic/connectives.lean | 2 +- library/logic/default.lean | 10 +++-- library/logic/eq.lean | 9 ++-- library/logic/identities.lean | 70 ++++++++++++++++--------------- library/logic/instances.lean | 5 --- library/logic/logic.md | 18 ++++---- library/logic/quantifiers.lean | 14 ++++--- library/logic/subsingleton.lean | 10 +++-- 10 files changed, 99 insertions(+), 82 deletions(-) diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index fa7256912..d951bd2f0 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -48,8 +48,8 @@ let u : {x | (∃y, P y) → P x} := has_property u Hex theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) : - P (@epsilon A (exists_imp_nonempty Hex) P) := -epsilon_spec_aux (exists_imp_nonempty Hex) P Hex + P (@epsilon A (nonempty_of_exists Hex) P) := +epsilon_spec_aux (nonempty_of_exists Hex) P Hex theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a := epsilon_spec (exists_intro a (eq.refl a)) @@ -60,7 +60,7 @@ epsilon_spec (exists_intro a (eq.refl a)) theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) : ∃f, ∀x, R x (f x) := -let f := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y), +let f := λx, @epsilon _ (nonempty_of_exists (H x)) (λy, R x y), H := take x, epsilon_spec (H x) in exists_intro f H diff --git a/library/logic/cast.lean b/library/logic/cast.lean index 396ef4c63..6291b7bb8 100644 --- a/library/logic/cast.lean +++ b/library/logic/cast.lean @@ -1,12 +1,16 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: cast.lean +Author: Leonardo de Moura + +Casts and heterogeneous equality. See also init.datatypes and init.logic. +-/ + import logic.eq logic.quantifiers open eq.ops --- cast.lean --- ========= - section universe variable u variables {A B : Type.{u}} @@ -30,20 +34,24 @@ namespace heq definition type_eq (H : a == b) : A = B := heq.rec_on H (eq.refl A) - theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ := + theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : + C b H₁ := rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁ theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b := drec_on H !cast_eq end heq -theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p := +theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : + eq.rec_on H p == p := eq.drec_on H !heq.refl section universe variables u v variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B} - theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : f a == f' a := + + theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : + f a == f' a := have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from take f f' H, heq.to_eq H ▸ heq.refl (f a), (H₂ ▸ aux) f f' H₁ @@ -105,10 +113,11 @@ section take H : P = P, heq.refl (eq.rec_on H f a), (H ▸ aux) H - theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) := + theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : + eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) := heq.to_eq (calc - eq.rec_on H f a == f a : rec_on_app H f a - ... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a))) + eq.rec_on H f a == f a : rec_on_app H f a + ... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a))) theorem cast_app (H : P = P') (f : Π x, P x) (a : A) : cast (pi_eq H) f a == f a := have H₁ : ∀ (H : (Π x, P x) = (Π x, P x)), cast H f a == f a, from @@ -116,7 +125,6 @@ section have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from H ▸ H₁, H₂ (pi_eq H) - end section @@ -144,7 +152,8 @@ section (Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' := heq.to_eq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd)) - --mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. Then proving eq is easier than proving heq) + -- mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. + -- Then proving eq is easier than proving heq) theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b') (Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c') : f a b c = f a' b' c' := diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index f8516abf8..c7b302424 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: logic.connectives Authors: Jeremy Avigad, Leonardo de Moura -The propositional connectives. See also init.datatypes. +The propositional connectives. See also init.datatypes and init.logic. -/ variables {a b c d : Prop} diff --git a/library/logic/default.lean b/library/logic/default.lean index 4d5618f4f..246901e26 100644 --- a/library/logic/default.lean +++ b/library/logic/default.lean @@ -1,6 +1,10 @@ ---- Copyright (c) 2014 Microsoft Corporation. All rights reserved. ---- Released under Apache 2.0 license as described in the file LICENSE. ---- Author: Jeremy Avigad +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: logic.default +Author: Jeremy Avigad +-/ import logic.eq logic.connectives logic.cast logic.subsingleton import logic.quantifiers logic.instances logic.identities diff --git a/library/logic/eq.lean b/library/logic/eq.lean index db7387743..ecb57f87a 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -1,16 +1,13 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. + +Module: logic.eq Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -Additional declarations/theorems about equality +Additional declarations/theorems about equality. See also init.datatypes and init.logic. -/ --- logic.eq --- ======== - --- Equality. - open eq.ops namespace eq diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 3aaa98477..6e4f50a0c 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -1,36 +1,37 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Jeremy Avigad, Leonardo de Moura +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. --- logic.identities --- ============================ +Module: logic.identities +Authors: Jeremy Avigad, Leonardo de Moura --- Useful logical identities. In the absence of propositional extensionality, some of the --- calculations use the type class support provided by logic.instances +Useful logical identities. Since we are not using propositional extensionality, some of the +calculations use the type class support provided by logic.instances. +-/ import logic.connectives logic.instances logic.quantifiers logic.cast open relation decidable relation.iff_ops -theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := +theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := calc (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc ... ↔ a ∨ (c ∨ b) : {or.comm} ... ↔ (a ∨ c) ∨ b : iff.symm or.assoc -theorem or_left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) := +theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) := calc a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc ... ↔ (b ∨ a) ∨ c : {or.comm} ... ↔ b ∨ (a ∨ c) : or.assoc -theorem and_right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b := +theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b := calc (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc ... ↔ a ∧ (c ∧ b) : {and.comm} ... ↔ (a ∧ c) ∧ b : iff.symm and.assoc -theorem and_left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) := +theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) := calc a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc ... ↔ (b ∧ a) ∧ c : {and.comm} @@ -46,14 +47,14 @@ iff.intro theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a := iff.mp not_not_iff H -theorem not_true_iff_false : (¬true) ↔ false := +theorem not_true_iff_false : ¬true ↔ false := iff.intro (assume H, H trivial) false.elim -theorem not_false_iff_true : (¬false) ↔ true := +theorem not_false_iff_true : ¬false ↔ true := iff.intro (assume H, trivial) (assume H H', H') theorem not_or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] : - (¬(a ∨ b)) ↔ (¬a ∧ ¬b) := + ¬(a ∨ b) ↔ ¬a ∧ ¬b := iff.intro (assume H, or.elim (em a) (assume Ha, absurd (or.inl Ha) H) @@ -65,7 +66,8 @@ iff.intro (assume Ha, absurd Ha (and.elim_left H)) (assume Hb, absurd Hb (and.elim_right H))) -theorem not_and {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) := +theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] : + ¬(a ∧ b) ↔ ¬a ∨ ¬b := iff.intro (assume H, or.elim (em a) (assume Ha, or.elim (em b) @@ -77,7 +79,7 @@ iff.intro (assume Hna, absurd (and.elim_left N) Hna) (assume Hnb, absurd (and.elim_right N) Hnb)) -theorem imp_or {a b : Prop} [Da : decidable a] : (a → b) ↔ (¬a ∨ b) := +theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b := iff.intro (assume H : a → b, (or.elim (em a) (assume Ha : a, or.inr (H Ha)) @@ -85,27 +87,29 @@ iff.intro (assume (H : ¬a ∨ b) (Ha : a), or_resolve_right H (not_not_iff⁻¹ ▸ Ha)) -theorem not_implies {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a → b)) ↔ (a ∧ ¬b) := -calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or} - ... ↔ (¬¬a ∧ ¬b) : not_or_iff_not_and_not - ... ↔ (a ∧ ¬b) : {not_not_iff} +theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] : + ¬(a → b) ↔ a ∧ ¬b := +calc + ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or} + ... ↔ ¬¬a ∧ ¬b : not_or_iff_not_and_not + ... ↔ a ∧ ¬b : {not_not_iff} theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a := assume H, by_contradiction (assume Hna : ¬a, have Hnna : ¬¬a, from not_not_of_not_implies (mt H Hna), absurd (not_not_elim Hnna) Hna) -theorem not_exists_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)] +theorem forall_not_of_not_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)] (H : ¬∃x, P x) : ∀x, ¬P x := take x, or.elim (em (P x)) (assume Hp : P x, absurd (exists_intro x Hp) H) (assume Hn : ¬P x, Hn) -theorem not_forall_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)] +theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)] [D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) : ∃x, ¬P x := @by_contradiction _ D' (assume H1 : ¬∃x, ¬P x, - have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not.decidable (D x)) H1, + have H2 : ∀x, ¬¬P x, from @forall_not_of_not_exists _ _ (take x, not.decidable (D x)) H1, have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x), absurd H3 H) @@ -119,32 +123,32 @@ iff.intro (assume H1 : a, absurd H1 H) (assume H2 : false, false.elim H2) -theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false := +theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false := iff.intro (assume H, false.of_ne H) (assume H, false.elim H) -theorem eq_id {A : Type} (a : A) : (a = a) ↔ true := +theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true := iff_true_intro rfl -theorem heq_id {A : Type} (a : A) : (a == a) ↔ true := +theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true := iff_true_intro (heq.refl a) -theorem a_iff_not_a (a : Prop) : (a ↔ ¬a) ↔ false := +theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false := iff.intro (assume H, have H' : ¬a, from assume Ha, (H ▸ Ha) Ha, H' (H⁻¹ ▸ H')) (assume H, false.elim H) -theorem true_eq_false : (true ↔ false) ↔ false := -not_true_iff_false ▸ (a_iff_not_a true) +theorem true_iff_false : (true ↔ false) ↔ false := +not_true_iff_false ▸ (iff_not_self true) -theorem false_eq_true : (false ↔ true) ↔ false := -not_false_iff_true ▸ (a_iff_not_a false) +theorem false_iff_true : (false ↔ true) ↔ false := +not_false_iff_true ▸ (iff_not_self false) -theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a := +theorem iff_true_iff (a : Prop) : (a ↔ true) ↔ a := iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H) -theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a := +theorem iff_false_iff_not (a : Prop) : (a ↔ false) ↔ ¬a := iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H) diff --git a/library/logic/instances.lean b/library/logic/instances.lean index 4b0853a8d..f5da26e7a 100644 --- a/library/logic/instances.lean +++ b/library/logic/instances.lean @@ -20,7 +20,6 @@ relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T) theorem is_equivalence_iff [instance] : relation.is_equivalence iff := relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans - /- congruences for logic operations -/ theorem is_congruence_not : is_congruence iff iff not := @@ -62,14 +61,12 @@ is_congruence2.mk (assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2)) (assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2)))) --- theorem is_congruence_const_iff [instance] := is_congruence.const iff iff.refl definition is_congruence_not_compose [instance] := is_congruence.compose is_congruence_not definition is_congruence_and_compose [instance] := is_congruence.compose21 is_congruence_and definition is_congruence_or_compose [instance] := is_congruence.compose21 is_congruence_or definition is_congruence_implies_compose [instance] := is_congruence.compose21 is_congruence_imp definition is_congruence_iff_compose [instance] := is_congruence.compose21 is_congruence_iff - /- a general substitution operation with respect to an arbitrary congruence -/ namespace general_subst @@ -77,13 +74,11 @@ namespace general_subst {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (is_congruence.app C H) H1 end general_subst - /- iff can be coerced to implication -/ definition mp_like_iff [instance] : relation.mp_like iff := relation.mp_like.mk (λa b (H : a ↔ b), iff.elim_left H) - /- support for calculations with iff -/ namespace iff diff --git a/library/logic/logic.md b/library/logic/logic.md index c86ef3c66..2a97b5dd8 100644 --- a/library/logic/logic.md +++ b/library/logic/logic.md @@ -1,22 +1,22 @@ logic ===== -Additional constructions and axioms. By default, `import logic` does not -import any axioms. +Logical constructions and theorems, beyond what has already been +declared in init.datatypes and init.logic. -Logical operations and connectives. +The subfolder logic.axioms declares additional axioms. The command +`import logic` does not import any axioms by default. +* [connectives](connectives.lean) : the propositional connectives * [eq](eq.lean) : additional theorems for equality and disequality * [cast](cast.lean) : casts and heterogeneous equality * [quantifiers](quantifiers.lean) : existential and universal quantifiers * [identities](identities.lean) : some useful identities +* [instances](instances.lean) : class instances for eq and iff +* [subsingleton](subsingleton.lean) +* [default](default.lean) -Constructively, inhabited types have a witness, while nonempty types -are "proof irrelevant". Classically (assuming the axioms in -logic.axioms.hilbert) the two are equivalent. Type class inferences -are set up to use "inhabited" however, so users should use that to -declare that types have an element. Use "nonempty" in the hypothesis -of a theorem when the theorem does not depend on the witness chosen. +Subfolders: * [axioms](axioms/axioms.md) : additional axioms * [examples](examples/examples.md) \ No newline at end of file diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index 7b01e7ed6..67847ca4a 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -4,16 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: logic.quantifiers Authors: Leonardo de Moura, Jeremy Avigad + +Universal and existential quantifiers. See also init.logic. -/ open inhabited nonempty -theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x := +theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x := assume H1 : ∀x, ¬p x, obtain (w : A) (Hw : p w), from H, absurd Hw (H1 w) -theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x := +theorem not_exists_not_of_forall {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x := assume H1 : ∃x, ¬p x, obtain (w : A) (Hw : ¬p w), from H1, absurd (H2 w) Hw @@ -41,12 +43,14 @@ iff.intro (assume Hl, obtain a Hp, from Hl, Hp) (assume Hr, inhabited.destruct H (take a, exists_intro a Hr)) -theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) := +theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : + (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) := iff.intro (assume H, and.intro (take x, and.elim_left (H x)) (take x, and.elim_right (H x))) (assume H, take x, and.intro (and.elim_left H x) (and.elim_right H x)) -theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) := +theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : + (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) := iff.intro (assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H, or.elim Hw @@ -58,7 +62,7 @@ iff.intro (assume H2, obtain (w : A) (Hw : ψ w), from H2, exists_intro w (or.inr Hw))) -theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A := +theorem nonempty_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A := obtain w Hw, from H, nonempty.intro w section diff --git a/library/logic/subsingleton.lean b/library/logic/subsingleton.lean index 2efb27125..0fe2e0ddc 100644 --- a/library/logic/subsingleton.lean +++ b/library/logic/subsingleton.lean @@ -1,8 +1,11 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn + +Module: logic.subsingleton +Author: Floris van Doorn -/ + import logic.eq inductive subsingleton [class] (A : Type) : Prop := @@ -28,7 +31,8 @@ subsingleton.intro (fun d1 d2, d2) d1) -protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} +protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p] + {H1 : p → Type} {H2 : ¬p → Type} (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h)) - : subsingleton (decidable.rec_on H H1 H2) := + : subsingleton (decidable.rec_on H H1 H2) := decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"