test(tests/lean/run/blast_cc8): add card based on finite_set test for congruence closure module

tests/lean/run/blast_cc8.lean

@@ -0,0 +1,43 @@
+import data.finset
+open set finset
+
+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)
+
+set_option blast.subst false
+set_option blast.simp  false
+
+/- 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