Commits

Paweł Wieczorek committed f3633cd

* wykasowanie plików automatycznie generowanych oraz śmieci

  • Participants
  • Parent commits 0eac99d

Comments (0)

Files changed (8)

File metalogic/Util/Ensemble_facts.v.d

-Util/Ensemble_facts.vo Util/Ensemble_facts.glob: Util/Ensemble_facts.v

File metalogic/Util/Finite_ensembles

-
-Require Import Sets.Finite_sets.
-Require Import Logic.Decidable.
-Require Import Sets.Ensembles.
-Require Import Set_calculus.
-
-Section S1.
-
-Variable U:Type.
-Variable A B C D: Ensemble U.
-Check eq.
-Variable decU: forall a b:U, decidable(eq a b).
-
-Lemma singleton_decidable (a:U) (x:U) : decidable (In _ (Singleton _ a) x).
-Proof.
- intros a x.
- destruct decU with a x.
- left. compute. rewrite H. apply In_singleton.
- right. intro. inversion H0. contradiction.
-Qed.
-
-
-Lemma finite_set_is_decidable: Finite _ A -> forall a, decidable (In _ A a).
-Proof.
-intros FA.
-induction FA.
-intros. right. intro. contradiction.
-intros.
- destruct IHFA with a.
- left. apply Union_introl. assumption.
- destruct decU with a x.
- left. apply Union_intror. rewrite H1. apply In_singleton.
- right. intro. destruct H2. contradiction. inversion H2. symmetry in H3.
- contradiction.
-Qed.
-
-
-End S1.
-
-Section S2.
-
-Variable U:Type.
-Variable A B C D: Ensemble U.
-Check eq.
-Variable decU: forall a b:U, decidable(eq a b).
-
-
-Lemma union_finite:
- Finite _ A -> Finite _ B -> Finite _ (Union _ A B).
-Proof.
- intros FA FB.
- induction FA.
- rewrite union_emptyl.
- assumption.
- unfold Add.
- rewrite union_AB_C_eq_AC_B.
- destruct finite_set_is_decidable with U B x.
- apply decU. assumption.
- replace (Union U (Union U A B) (Singleton U x))
-  with (Add _ (Union _ A B) x).
- rewrite set_add_same.
- apply IHFA. apply Union_intror. assumption.
- auto.
-
- assert (~(In U (Union _ A B) x)).
- intro. destruct H1. contradiction. contradiction.
- apply Union_is_finite. assumption. assumption.
-Qed.
-
-End S2.
-

File metalogic/Util/Finite_ensembles.

-
-Require Import Sets.Finite_sets.
-Require Import Logic.Decidable.
-Require Import Sets.Ensembles.
-Require Import Set_calculus.
-
-Section S1.
-
-Variable U:Type.
-Variable A B C D: Ensemble U.
-Check eq.
-Variable decU: forall a b:U, decidable(eq a b).
-
-Lemma singleton_decidable (a:U) (x:U) : decidable (In _ (Singleton _ a) x).
-Proof.
- intros a x.
- destruct decU with a x.
- left. compute. rewrite H. apply In_singleton.
- right. intro. inversion H0. contradiction.
-Qed.
-
-
-Lemma finite_set_is_decidable: Finite _ A -> forall a, decidable (In _ A a).
-Proof.
-intros FA.
-induction FA.
-intros. right. intro. contradiction.
-intros.
- destruct IHFA with a.
- left. apply Union_introl. assumption.
- destruct decU with a x.
- left. apply Union_intror. rewrite H1. apply In_singleton.
- right. intro. destruct H2. contradiction. inversion H2. symmetry in H3.
- contradiction.
-Qed.
-
-
-End S1.
-
-Section S2.
-
-Variable U:Type.
-Variable A B C D: Ensemble U.
-Check eq.
-Variable decU: forall a b:U, decidable(eq a b).
-
-
-Lemma union_finite:
- Finite _ A -> Finite _ B -> Finite _ (Union _ A B).
-Proof.
- intros FA FB.
- induction FA.
- rewrite union_emptyl.
- assumption.
- unfold Add.
- rewrite union_AB_C_eq_AC_B.
- destruct finite_set_is_decidable with U B x.
- apply decU. assumption.
- replace (Union U (Union U A B) (Singleton U x))
-  with (Add _ (Union _ A B) x).
- rewrite set_add_same.
- apply IHFA. apply Union_intror. assumption.
- auto.
-
- assert (~(In U (Union _ A B) x)).
- intro. destruct H1. contradiction. contradiction.
- apply Union_is_finite. assumption. assumption.
-Qed.
-
-End S2.
-

File metalogic/Util/Laws.v.d

-Util/Laws.vo Util/Laws.glob: Util/Laws.v

File metalogic/Util/List_facts.v.d

-Util/List_facts.vo Util/List_facts.glob: Util/List_facts.v

File metalogic/Util/Seq.v.d

-Util/Seq.vo Util/Seq.glob: Util/Seq.v

File metalogic/Util/Set_calculus.v.d

-Util/Set_calculus.vo Util/Set_calculus.glob: Util/Set_calculus.v

File metalogic/Util/Theory.v.d

-Util/Theory.vo Util/Theory.glob: Util/Theory.v ./Pc/Lang.vo ./Pc/Proof.vo ./Pc/Proof_facts.vo