Merge PR #17940: Briefly rewritten proofs of Finite_sets_facts.v

Reviewed-by: olaure01 Co-authored-by: olaure01 <olaure01@users.noreply.github.com>
coq · Sep 20, 2023 · 2db45f6 · 2db45f6
2 parents 83a06f3 + d3f9053
commit 2db45f6
Showing 1 changed file with 87 additions and 190 deletions.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
@@ -62,33 +62,30 @@ Section Finite_sets_facts.
 
   Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
   Proof.
-    intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
-    change (Finite U (Add U (Empty_set U) x)); auto with sets.
+    intro x; rewrite <- Empty_set_zero'.
+    apply Union_is_finite; auto with sets.
   Qed.
 
   Theorem Union_preserves_Finite :
     forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
   Proof.
-    intros X Y H; induction H as [|A Fin_A Hind x].
-    - rewrite (Empty_set_zero U Y). trivial.
-    - intros.
-      rewrite (Union_commutative U (Add U A x) Y).
-      rewrite <- (Union_add U Y A x).
-      rewrite (Union_commutative U Y A).
+    intros X Y HX HY.
+    induction HX.
+    - now rewrite Empty_set_zero.
+    - rewrite Union_commutative.
+      rewrite <- Union_add.
       apply Add_preserves_Finite.
-      apply Hind. assumption.
+      now rewrite Union_commutative.
   Qed.
 
   Lemma Finite_downward_closed :
     forall A:Ensemble U,
       Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
   Proof.
-    intros A H'; elim H'; auto with sets.
-    - intros X H'0.
-      rewrite (less_than_empty U X H'0); auto with sets.
-    - intros; elim Included_Add with U X A0 x; auto with sets.
-      destruct 1 as [A' [H5 H6]].
-      rewrite H5; auto with sets.
+    intros A HA.
+    induction HA as [|A HA IHHA]; [ intros X HX | intros X HXAx ].
+    - rewrite less_than_empty; auto with sets.
+    - destruct (Included_Add _ _ _ _ HXAx) as [|[X' [-> HX'A]]]; auto with sets.
   Qed.
 
   Lemma Intersection_preserves_finite :
@@ -107,50 +104,35 @@ Section Finite_sets_facts.
   Lemma inh_card_gt_O :
     forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
   Proof.
-    induction 1 as [x H'].
-    intros n H'0.
-    destruct n; [ exfalso | apply Nat.lt_0_succ ].
-    rewrite (cardinalO_empty X) in H'; [ elim H' | assumption ].
+    intros X [x HX] [] HCX.
+    - now rewrite (cardinalO_empty X HCX) in HX.
+    - apply Nat.lt_0_succ.
   Qed.
 
   Lemma card_soustr_1 :
     forall (X:Ensemble U) (n:nat),
       cardinal U X n ->
       forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
   Proof.
-    intros X n H'; elim H'.
-    - intros x H'0; elim H'0.
-    - clear H' n X.
-      intros X n H' H'0 x H'1 x0 H'2.
-      elim (classic (In U X x0)).
-      + intro H'4; rewrite (add_soustr_xy U X x x0).
-        * elim (classic (x = x0)).
-          -- intro H'5.
-             absurd (In U X x0); auto with sets.
-             rewrite <- H'5; auto with sets.
-          -- intro H'3; try assumption.
-             cut (S (pred n) = pred (S n)).
-             ++ intro H'5; rewrite <- H'5.
-                apply card_add; auto with sets.
-                red; intro H'6; elim H'6.
-                intros H'7 H'8; try assumption.
-                elim H'1; auto with sets.
-             ++ unfold pred at 2.
-                apply (Nat.lt_succ_pred 0).
-                apply inh_card_gt_O with (X := X); auto with sets.
-                apply Inhabited_intro with (x := x0); auto with sets.
-        * red; intro H'3.
-          apply H'1.
-          elim H'3; auto with sets.
-          rewrite H'3; auto with sets.
-      + elim (classic (x = x0)).
-        * intro H'3; rewrite <- H'3.
-          cut (Subtract U (Add U X x) x = X); auto with sets.
-          intro H'4; rewrite H'4; auto with sets.
-        * intros H'3 H'4; try assumption.
-          absurd (In U (Add U X x) x0); auto with sets.
-          red; intro H'5; try exact H'5.
-          lapply (Add_inv U X x x0); tauto.
+    intros X n H. induction H as [|X n H IH x Hx]; intros x' Hx'.
+    - destruct Hx'.
+    - rewrite Nat.pred_succ.
+      apply Add_inv in Hx' as [Hx' | <-].
+      + rewrite (add_soustr_xy _ _ x x') by (intros <-; contradiction Hx).
+        rewrite <- Nat.succ_pred_pos.
+        * apply card_add; [ apply (IH _ Hx') |].
+          now intros [? _]%Subtract_inv.
+        * apply inh_card_gt_O with (X := X); [| assumption ].
+          exact (Inhabited_intro _ _ _ Hx').
+      + rewrite <- (Sub_Add_new _ _ _ Hx). assumption.
+  Qed.
+
+  Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
+  Proof.
+    intros m Cm.
+    inversion Cm as [|X n _ x _ H]; [ reflexivity | ].
+    symmetry in H.
+    now apply not_Empty_Add in H.
   Qed.
 
   Lemma cardinal_is_functional :
@@ -159,70 +141,41 @@ Section Finite_sets_facts.
       forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
   Proof.
     intros X c1 H'; elim H'.
-    - intros Y c2 H'0; elim H'0; auto with sets.
-      intros A n H'1 H'2 x H'3 H'5.
-      elim (not_Empty_Add U A x); auto with sets.
+    - intros Y c2 H'0 <-; now apply cardinal_Empty.
     - clear H' c1 X.
       intros X n H' H'0 x H'1 Y c2 H'2.
       elim H'2.
-      + intro H'3.
-        elim (not_Empty_Add U X x); auto with sets.
+      + intro H'3; now elim (not_Empty_Add U X x).
       + clear H'2 c2 Y.
-        intros X0 c2 H'2 H'3 x0 H'4 H'5.
-        elim (classic (In U X0 x)).
-        * intro H'6; apply f_equal.
-          apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-          -- assert (pred (S c2) = c2) as []; auto with sets.
-             apply card_soustr_1; auto with sets.
-          -- rewrite <- H'5.
-             apply Sub_Add_new; auto with sets.
-        * elim (classic (x = x0)).
-          -- intros H'6 H'7; apply f_equal.
-             apply H'0 with (Y := X0); auto with sets.
-             apply Simplify_add with (x := x); auto with sets.
-             pattern x at 2; rewrite H'6; auto with sets.
-          -- intros H'6 H'7.
-             absurd (Add U X x = Add U X0 x0); auto with sets.
-             clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-             red; intro H'.
-             lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
-             clear H'.
-             intro H'; red in H'.
-             elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
-             absurd (In U (Add U X0 x0) x); auto with sets.
-             lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
-  Qed.
-
-  Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
-  Proof.
-    intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
-    elim m; auto with sets.
-    intros; elim H0; intros; elim H1; intros; elim H2; intros.
-    elim (not_Empty_Add U x x0 H3).
+        intros X0 c2 H'2 _ x0 H'4 H'5.
+        apply f_equal.
+        assert (H'6 : In U (Add U X x) x) by apply Add_intro2.
+        rewrite H'5 in H'6.
+        destruct (Add_inv _ _ _ _ H'6) as [H'7 | <-].
+        * apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+          -- rewrite <- Nat.pred_succ; apply card_soustr_1; auto with sets.
+          -- rewrite <- H'5; auto with sets.
+        * apply (H'0 _ _ H'2 (Simplify_add _ _ _ _ H'1 H'4 H'5)).
   Qed.
 
   Lemma cardinal_unicity :
     forall (X:Ensemble U) (n:nat),
       cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
   Proof.
-    intros; apply cardinal_is_functional with X X; auto with sets.
+    intros X ? ? ? ?; now apply cardinal_is_functional with X X.
   Qed.
 
   Lemma card_Add_gen :
     forall (A:Ensemble U) (x:U) (n n':nat),
       cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
   Proof.
-    intros A x n n' H'.
-    elim (classic (In U A x)).
-    - intro H'0.
-      rewrite (Non_disjoint_union U A x H'0).
-      intro H'1; cut (n = n').
-      + intro E; rewrite E; auto with sets.
-      + apply cardinal_unicity with A; auto with sets.
-    - intros H'0 H'1.
-      cut (n' = S n).
-      + intro E; rewrite E; auto with sets.
-      + apply cardinal_unicity with (Add U A x); auto with sets.
+    intros A x n n' H0 H1.
+    elim (classic (In U A x)); intro H2.
+    - rewrite (Non_disjoint_union _ _ _ H2) in H1.
+      rewrite (cardinal_unicity _ _ H0 _ H1).
+      apply Nat.le_succ_diag_r.
+    - apply Nat.eq_le_incl.
+      apply cardinal_unicity with (X := Add U A x); auto with sets.
   Qed.
 
   Lemma incl_st_card_lt :
@@ -231,109 +184,53 @@ Section Finite_sets_facts.
       forall (Y:Ensemble U) (c2:nat),
 	cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
   Proof.
-    intros X c1 H'; elim H'.
-    - intros Y c2 H'0; elim H'0; [ | intros; apply Nat.lt_0_succ ].
-      intro H'1.
-      elim (Strict_Included_strict U (Empty_set U)); auto.
-    - clear H' c1 X.
-      intros X n H' H'0 x H'1 Y c2 H'2.
-      elim H'2.
-      + intro H'3; elim (not_SIncl_empty U (Add U X x)); assumption.
-      + clear H'2 c2 Y.
-        intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
-        * intro H'6; apply -> Nat.succ_lt_mono.
-          apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-          -- assert (pred (S c2) = c2) as []; [ reflexivity | ].
-             apply card_soustr_1; auto with sets.
-          -- apply incl_st_add_soustr; assumption.
-        * elim (classic (x = x0)).
-          -- intros H'6 H'7; apply -> Nat.succ_lt_mono.
-             apply H'0 with (Y := X0); [ assumption | ].
-             apply sincl_add_x with (x := x0).
-             ++ rewrite <- H'6; assumption.
-             ++ pattern x0 at 1; rewrite <- H'6; trivial.
-          -- intros H'6 H'7; red in H'5.
-             elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
-             red in H'8.
-             generalize (H'8 x).
-             intro H'5; lapply H'5; auto with sets.
-             intro H; elim Add_inv with U X0 x0 x; [ | | assumption ].
-             ++ intro; absurd (In U X0 x); assumption.
-             ++ intro; absurd (x = x0); [ assumption | subst x0; reflexivity ].
+    intros X c1 H1.
+    induction H1 as [|X' ? HX' IH x Hx]; intros Y c2 HY Hsincl;
+      (inversion HY as [HXY Hc | ? ? ? ? ? HXY]; subst Y; [ apply not_SIncl_empty in Hsincl as [] |]).
+    - apply Nat.lt_0_succ.
+    - subst c2. apply -> Nat.succ_lt_mono.
+      refine (IH _ _ _ (incl_st_add_soustr _ _ _ _ Hx Hsincl)).
+      rewrite <- Nat.pred_succ. apply card_soustr_1; [ assumption | ].
+      apply Hsincl, Add_intro2.
   Qed.
 
   Lemma incl_card_le :
     forall (X Y:Ensemble U) (n m:nat),
       cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
   Proof.
-    intros; elim Included_Strict_Included with U X Y; [ | | assumption ]; intro.
-    - cut (m > n); [ apply Nat.lt_le_incl | ].
-      apply incl_st_card_lt with (X := X) (Y := Y); assumption.
-    - generalize H0; rewrite <- H2; intro.
-      cut (n = m).
-      + intro E; rewrite E; auto with sets.
-      + apply cardinal_unicity with X; assumption.
-  Qed.
-
-  Lemma G_aux :
-    forall P:Ensemble U -> Prop,
-      (forall X:Ensemble U,
-	Finite U X ->
-	(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
-      P (Empty_set U).
-  Proof.
-    intros P H'; try assumption.
-    apply H'; auto with sets.
-    clear H'; auto with sets.
-    intros Y H'; try assumption.
-    red in H'.
-    elim H'; intros H'0 H'1; try exact H'1; clear H'.
-    lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
-    elim H'1; auto with sets.
+    intros X Y n m HX HY HXY.
+    destruct (Included_Strict_Included _ _ _ HXY) as [HXY' | <-].
+    - apply Nat.lt_le_incl.
+      now apply (incl_st_card_lt _ _ HX _ _ HY).
+    - apply Nat.eq_le_incl.
+      now apply cardinal_unicity with X.
   Qed.
 
   Lemma Generalized_induction_on_finite_sets :
     forall P:Ensemble U -> Prop,
       (forall X:Ensemble U,
-	Finite U X ->
-	(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+        Finite U X ->
+        (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
       forall X:Ensemble U, Finite U X -> P X.
   Proof.
-    intros P H'0 X H'1.
-    generalize P H'0; clear H'0 P.
-    elim H'1.
-    - intros P H'0.
-      apply G_aux; auto with sets.
-    - clear H'1 X.
-      intros A H' H'0 x H'1 P H'3.
-      cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
-      generalize H'1.
-      apply H'0.
-      intros X K H'5 L Y H'6; apply H'3; auto with sets.
-      + apply Finite_downward_closed with (A := Add U X x); auto with sets.
-      + intros Y0 H'7.
-        elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
-          auto with sets.
-        intros H'2 H'4.
-        elim (Included_Add U Y0 X x);
-          [ intro H'14
-          | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
-          | idtac ]; auto with sets.
-        * elim (Included_Strict_Included U Y0 X); auto with sets.
-          -- intro H'9; apply H'5 with (Y := Y0); auto with sets.
-          -- intro H'9; rewrite H'9.
-             apply H'3; auto with sets.
-             intros Y1 H'8; elim H'8.
-             intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
-        * elim (Included_Strict_Included U A' X); auto with sets.
-          -- intro H'8; apply H'5 with (Y := A'); auto with sets.
-             rewrite <- H'15; auto with sets.
-          -- intro H'8.
-             elim H'7.
-             intros H'9 H'10; apply H'10 || elim H'10; try assumption.
-             generalize H'6.
-             rewrite <- H'8.
-             rewrite <- H'15; auto with sets.
+    intros P HP X HX.
+    induction HX as [|X HX IH x Hx] in P, HP.
+    - apply HP; [ auto with sets | ].
+      now intros Y [->%less_than_empty []].
+    - enough (forall Y, Included U Y (Add U X x) -> P Y) by auto with sets.
+      revert Hx. apply IH. clear IH X HX.
+      intros Y HY IH' Hx Z HZYx.
+      apply HP; [ apply Finite_downward_closed with (Add _ Y x); auto with sets | ].
+      intros Z' HZ'Z.
+      pose proof (Strict_inclusion_is_transitive_with_inclusion _ _ _ _ HZ'Z HZYx) as [HZ'Yx Hneq].
+      case (Included_Add _ _ _ _ HZ'Yx) as [HZ'Y | [Y' [-> HY'Y]]].
+      + case (classic (Z' = Y)) as [-> | Hneq'].
+        * apply (HP _ HY).
+          intros Y' [HY'Y Hneq'].
+          apply (IH' Y'); auto with sets.
+        * apply (IH' Z'); auto with sets.
+      + apply (IH' Y'); auto with sets.
+        now split; [| intros -> ].
   Qed.
 
 End Finite_sets_facts.