feat(tests/lean/run/finset): show that if A has decidable equality, then (finset A) also has it.

tests/lean/run/finset.lean

@@ -1,31 +1,116 @@
-import logic.axioms.extensional data.list
-open list setoid quot
+import data.list
+open list setoid quot decidable nat
 
 namespace finset
 
   definition eqv {A : Type} (l₁ l₂ : list A) :=
   ∀ a, a ∈ l₁ ↔ a ∈ l₂
 
-  infix `∼` := eqv
+  infix `~` := eqv
 
-  theorem eqv.refl {A : Type} (l : list A) : l ∼ l :=
+  theorem eqv.refl {A : Type} (l : list A) : l ~ l :=
   λ a, !iff.refl
 
-  theorem eqv.symm {A : Type} {l₁ l₂ : list A} : l₁ ∼ l₂ → l₂ ∼ l₁ :=
+  theorem eqv.symm {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₂ ~ l₁ :=
   λ H a, iff.symm (H a)
 
-  theorem eqv.trans {A : Type} {l₁ l₂ l₃ : list A} : l₁ ∼ l₂ → l₂ ∼ l₃ → l₁ ∼ l₃ :=
+  theorem eqv.trans {A : Type} {l₁ l₂ l₃ : list A} : l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ :=
   λ H₁ H₂ a, iff.trans (H₁ a) (H₂ a)
 
   theorem eqv.is_equivalence (A : Type) : equivalence (@eqv A) :=
   and.intro (@eqv.refl A) (and.intro (@eqv.symm A) (@eqv.trans A))
 
+  definition norep {A : Type} [H : decidable_eq A] : list A → list A
+  | []        :=  []
+  | (x :: xs) :=  if x ∈ xs then norep xs else x :: norep xs
+
+  definition eqv_norep {A : Type} [H : decidable_eq A] : ∀ l : list A, l ~ norep l
+  | []        := (λ a, iff.rfl)
+  | (x :: xs) :=
+    take y,
+    show y ∈ x :: xs ↔ y ∈ if x ∈ xs then norep xs else x :: norep xs,
+    begin
+      apply (@by_cases (x ∈ xs)),
+      begin
+        intro xin, rewrite (if_pos xin),
+        apply iff.intro,
+        {intro yinxxs, apply (or.elim (iff.mp !mem_cons_iff yinxxs)),
+          intro yeqx,  rewrite -yeqx at xin, exact (iff.mp (eqv_norep xs y) xin),
+          intro yeqxs, exact (iff.mp (eqv_norep xs y) yeqxs)},
+        {intro yinnrep, show y ∈ x::xs, from or.inr (iff.mp' (eqv_norep xs y) yinnrep)}
+      end,
+      begin
+        intro xnin, rewrite (if_neg xnin),
+        apply iff.intro,
+        {intro yinxxs, apply (or.elim (iff.mp !mem_cons_iff yinxxs)),
+          intro yeqx, rewrite yeqx, apply mem_cons,
+          intro yinxs, show y ∈ x:: norep xs, from or.inr (iff.mp (eqv_norep xs y) yinxs)},
+        {intro yinxnrep, apply (or.elim (iff.mp !mem_cons_iff yinxnrep)),
+          intro yeqx, rewrite yeqx, apply mem_cons,
+          intro yinrep, show y ∈ x::xs, from or.inr (iff.mp' (eqv_norep xs y) yinrep)}
+      end
+    end
+
+  definition sub {A : Type} (l₁ l₂ : list A) := ∀ a, a ∈ l₁ → a ∈ l₂
+
+  infix ⊆ := sub
+
+  theorem eqv_of_sub_of_sub {A : Type} {l₁ l₂ : list A} : l₁ ⊆ l₂ → l₂ ⊆ l₁ → l₁ ~ l₂ :=
+  assume h₁ h₂ a, iff.intro (h₁ a) (h₂ a)
+
+  theorem sub_of_eqv_left {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₁ ⊆ l₂ :=
+  assume h₁ a ainl₁, iff.mp (h₁ a) ainl₁
+
+  theorem sub_of_eqv_right {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₂ ⊆ l₁ :=
+  assume h₁ a ainl₂, iff.mp' (h₁ a) ainl₂
+
+  definition sub_of_cons_sub {A : Type} {a : A} {l₁ l₂ : list A} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
+  assume s, take b, assume binl₁, s b (or.inr binl₁)
+
+  definition decidable_sub [instance] {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ ⊆ l₂)
+  | []      ys      := inl (λ a h, absurd h !not_mem_nil)
+  | (x::xs) ys      :=
+    if xinys : x ∈ ys then
+      match decidable_sub xs ys with
+      | (inl xs_sub_ys)  := inl (λ y yinxxs, or.elim (iff.mp !mem_cons_iff yinxxs)
+         (λ yeqx, by rewrite yeqx; exact xinys)
+         (λ yinxs, xs_sub_ys y yinxs))
+      | (inr nxs_sub_ys) := inr (λ h, absurd (sub_of_cons_sub h) nxs_sub_ys)
+      end
+    else
+      inr (λ h, absurd (h x !mem_cons) xinys)
+
+  example : [(1 : nat), 2, 3] ⊆ [1,3,4,1,2] :=
+  dec_trivial
+
+  definition decidable_eqv [instance] {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ ~ l₂) :=
+  take l₁ l₂ : list A,
+  match decidable_sub l₁ l₂ with
+  | (inl s₁) :=
+    match decidable_sub l₂ l₁ with
+    | (inl s₂) := inl (eqv_of_sub_of_sub s₁ s₂)
+    | (inr n₂) := inr (λ h, absurd (sub_of_eqv_right h) n₂)
+    end
+  | (inr n₁) := inr (λ h, absurd (sub_of_eqv_left h) n₁)
+  end
+
+  example : [(1:nat), 2, 3, 2, 2, 2] ~ [1,3,3,1,2] :=
+  dec_trivial
+
   definition finset_setoid [instance] (A : Type) : setoid (list A) :=
   setoid.mk (@eqv A) (eqv.is_equivalence A)
 
   definition finset (A : Type) : Type :=
   quot (finset_setoid A)
 
+  definition has_decidable_eq [instance] {A : Type} [H : decidable_eq A] : ∀ s₁ s₂ : finset A, decidable (s₁ = s₂) :=
+  take s₁ s₂, quot.rec_on_subsingleton₂ s₁ s₂
+   (take l₁ l₂,
+      match decidable_eqv l₁ l₂ with
+      | inl e := inl (quot.sound e)
+      | inr d := inr (λ e, absurd (quot.exact e) d)
+      end)
+
   definition to_finset {A : Type} (l : list A) : finset A :=
   ⟦l⟧
 
@@ -60,6 +145,7 @@ namespace finset
         end,
         begin
           intro inl₃l₄,
+
           apply (or.elim (mem_or_mem_of_mem_append inl₃l₄)),
           intro inl₃, exact (mem_append_of_mem_or_mem (or.inl (iff.mp' (r₁ a) inl₃))),
           intro inl₄, exact (mem_append_of_mem_or_mem (or.inr (iff.mp' (r₂ a) inl₄)))
@@ -83,4 +169,10 @@ namespace finset
   example : to_finset (1::2::nil) ∪ to_finset (2::3::nil) = ⟦1 :: 2 :: 2 :: 3 :: nil⟧ :=
   rfl
 
+  example : to_finset [(1:nat), 1, 2, 3] = to_finset [2, 3, 1, 2, 2, 3] :=
+  dec_trivial
+
+  example : to_finset [(1:nat), 1, 4, 2, 3] ≠ to_finset [2, 3, 1, 2, 2, 3] :=
+  dec_trivial
+
 end finset