2015-11-28 23:01:10 +00:00
|
|
|
-- Testing all possible cases of [unit_action]
|
2015-12-07 16:45:54 +00:00
|
|
|
set_option blast.strategy "unit"
|
|
|
|
|
|
2015-11-28 23:01:10 +00:00
|
|
|
universes l1 l2
|
|
|
|
|
variables {A B C : Prop}
|
|
|
|
|
variables {X : Type.{l1}} {Y : Type.{l2}}
|
|
|
|
|
variables {P : Y → Prop}
|
|
|
|
|
|
|
|
|
|
-- Types as antecedents
|
|
|
|
|
example (H : X → A) (x : X) : A := by blast
|
|
|
|
|
example (H : X → A → B) (x : X) (nb : ¬ B) : ¬ A := by blast
|
|
|
|
|
example (H : A → X → B → C) (x : X) (a : A) (nc : ¬ C) : ¬ B := by blast
|
|
|
|
|
|
|
|
|
|
-- Universally quantified facts
|
|
|
|
|
example (H : A → X → B → ∀ y : Y, P y) (x : X) (a : A) (nc : ¬ ∀ y : Y, P y) : ¬ B := by blast
|
|
|
|
|
example (H : A → X → B → ¬ ∀ y : Y, P y) (x : X) (a : A) (nc : ∀ y : Y, P y) : ¬ B := by blast
|
