2015-12-06 07:52:16 +00:00
|
|
|
|
import data.finset data.set
|
2015-11-21 23:02:50 +00:00
|
|
|
|
open set finset
|
2015-12-06 22:33:21 +00:00
|
|
|
|
set_option blast.strategy "cc"
|
2015-11-21 23:02:50 +00:00
|
|
|
|
|
|
|
|
|
|
structure finite_set [class] {T : Type} (xs : set T) :=
|
|
|
|
|
|
(to_finset : finset T) (is_equiv : to_set to_finset = xs)
|
|
|
|
|
|
|
|
|
|
|
|
definition finset_set.is_subsingleton [instance] (T : Type) (xs : set T) : subsingleton (finite_set xs) :=
|
|
|
|
|
|
begin
|
|
|
|
|
|
constructor, intro a b,
|
|
|
|
|
|
induction a with f₁ h₁,
|
|
|
|
|
|
induction b with f₂ h₂,
|
|
|
|
|
|
subst xs,
|
|
|
|
|
|
let e := to_set.inj h₂,
|
|
|
|
|
|
subst e
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
/- Add some instances for finite_sets -/
|
|
|
|
|
|
variable {A : Type}
|
|
|
|
|
|
definition finite_set_empty [instance] : finite_set (∅:set A) := sorry
|
|
|
|
|
|
definition finite_set_finset [instance] (fxs : finset A) : finite_set (to_set fxs) := sorry
|
|
|
|
|
|
definition finite_set_insert [instance] (xs : set A) [fxs : finite_set xs] (x : A) : finite_set (insert x xs) := sorry
|
|
|
|
|
|
definition finite_set_union [instance] (xs : set A) [fxs : finite_set xs] (ys : set A) [fys : finite_set ys] : finite_set (xs ∪ ys) := sorry
|
|
|
|
|
|
definition finite_set_inter1 [instance] (xs : set A) [fxs : finite_set xs] (ys : set A) [ys_dec : decidable_pred ys] : finite_set (xs ∩ ys) := sorry
|
|
|
|
|
|
definition finite_set_inter2 [instance] (xs : set A) [fxs : finite_set xs] (ys : set A) [ys_dec : decidable_pred ys] : finite_set (ys ∩ xs) := sorry
|
|
|
|
|
|
definition finite_set_set_of [instance] (xs : set A) [fxs : finite_set xs] : finite_set (set.set_of xs) := sorry
|
|
|
|
|
|
|
|
|
|
|
|
/- Defined cardinality using finite_set type class -/
|
|
|
|
|
|
noncomputable definition mycard {T : Type} (xs : set T) [fxs : finite_set xs] :=
|
|
|
|
|
|
finset.card (to_finset xs)
|
|
|
|
|
|
|
|
|
|
|
|
/- Congruence closure still works :-) -/
|
|
|
|
|
|
definition tst
|
|
|
|
|
|
(A : Type) (s₁ s₂ s₃ s₄ s₅ s₆ : set A)
|
|
|
|
|
|
[fxs₁ : finite_set s₁] [fxs₂ : finite_set s₂]
|
|
|
|
|
|
[fxs₁ : finite_set s₃] [fxs₂ : finite_set s₄]
|
|
|
|
|
|
[d₁ : decidable_pred s₅] [d₂ : decidable_pred s₆] :
|
|
|
|
|
|
s₁ = s₂ → s₃ = s₄ → s₆ = s₅ → mycard ((s₁ ∪ s₃) ∩ s₅) = mycard ((s₂ ∪ s₄) ∩ s₆) :=
|
|
|
|
|
|
by blast
|
|
|
|
|
|
|
|
|
|
|
|
print tst
|
