here is the full code. The problem is in lemma Th5.
Require
Import Relation_Definitions.
Require Import Coq.Program.Basics.
Require Import Coq.Classes.EquivDec.
Require Import Coq.Program.Tactics.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Classes.SetoidTactics.
Require Import Coq.Logic.Decidable.
Require Import Unicode.Utf8.
Require Import Coq.Logic.Classical_Prop.
Section Mereo.
Universe Name.
Variable name : Type@{Name}.
Variable plural : Type@{Name}.
Variable particular : Type@{Name}.
Variable c01 : plural -> name. Coercion c01 : plural
>-> name.
Variable c02 : particular -> name. Coercion c02 :
particular >-> name.
Inductive eps :particular -> name -> Prop :=
| particularEquality: forall(A:particular)(B:particular), eps
A B
| epsilon : forall(A:particular)(b:plural), eps A b.
Notation "A 'ε' b" := (eps A b) (at level 40).
Definition Eq_name (a b:name) := @eq name a b.
Variable Λ : plural.
Variable Ω : plural.
Axiom contra_name : forall (A:particular), A ε Λ <->
False.
Axiom A_is_object : forall (A:particular), A ε Ω <->
True.
Axiom A01 : forall (A:particular), A ε A. (* reflexivity *)
Axiom A02 : forall (A B C:particular), (A ε B /\ C ε B) ->
A ε C.
Axiom A03 : forall (A:particular)(a:plural), A ε a <->
forall D, (D ε A -> D ε a).
Axiom A04 : forall (A:particular), A ε A -> exists
b:plural, A ε b.
Lemma Ax01 : forall (A:particular)(a:plural), A ε a ->
(exists B:particular, B ε A).
Proof.
intros.
exists A.
apply A01.
Qed.
Lemma Equiv_Lesniewski_axiom_right : forall
(A:particular)(a:plural), A ε a -> (exists B:particular, B
ε A) /\
(forall (C
D:particular), (D ε A /\ C ε A) -> D ε C) /\
forall (D:particular),
D ε A -> D ε a.
Proof.
intros A b H1.
split.
+ apply (Ax01 A b);assumption.
+ split.
- intros;apply (A02 D A C);assumption.
- intros B H2;rewrite (A03 A b) in H1;specialize (H1
B);apply H1 in H2;assumption.
Qed.
Lemma Equiv_Lesniewski_axiom_left : forall
(A:particular)(a:plural), ((exists B:particular, B ε A) /\
(forall (C
D:particular), (D ε A /\ C ε A) -> D ε C) /\
forall (K:particular),
(K ε A -> K ε a)) -> A ε a.
Proof.
intros A a H1.
destruct H1 as [H1 H2].
destruct H2 as [H2 H3].
specialize (H3 A).
apply H3.
apply A01.
Qed.
Theorem Equiv_Lesniewski_axiom : forall
(A:particular)(a:plural), A ε a <-> (exists
B:particular, B ε A) /\
(forall (C
D:particular), (D ε A /\ C ε A) -> D ε C) /\
forall (K:particular),
K ε A -> K ε a.
Proof.
intros A a.
split.
- apply (Equiv_Lesniewski_axiom_right A a).
- eapply (Equiv_Lesniewski_axiom_left A a).
Qed.
(* ======================== particular equality
===============================*)
Lemma Tpart1 : forall A B:particular, B ε A -> A ε B. (*
symmetry *)
Proof.
intros A B H1.
assert (H2:A ε A).
- apply A01.
- assert (H4:=H2);apply (A02 A A B);split;assumption.
Qed.
Lemma Tpart2 : forall A B C:particular, A ε B -> B ε C
-> A ε C. (* transitivity *)
Proof.
intros A B C H1 H3.
apply (Tpart1 C B) in H3.
apply (A02 A B C).
split;assumption.
Qed.
Axiom eqpart : forall (A B:particular), A ε B /\ B ε A
<-> Eq_name A B.
Lemma eqpart_dec : forall pa1 pa2:particular, pa1 = pa2 \/
~(pa1 = pa2).
Proof.
intros x y.
apply classic.
Qed.
Definition weakInclusion (a b :plural) := forall A:particular,
A ε a -> A ε b.
Notation "a '⊆' b" := (weakInclusion a b) (at level 40).
Lemma LO1 : forall (A:particular)(a:plural), A ε a ->
exists B:particular, (B ε A /\ B ε a).
Proof.
intros A a H.
exists A.
split.
- apply A01.
- assumption.
Qed.
(* characteristic thesis of LO *)
Lemma LO6 : forall (A B:particular)(a:plural), B ε A /\ A ε a
-> A ε B.
Proof.
intros A B a H1.
destruct H1 as [H1 H2].
apply Tpart1 in H1.
assumption.
Qed.
Lemma LO7 : forall (A B:particular)(a:plural), A ε B /\ B ε a
-> A ε a.
Proof.
intros A B a H1.
destruct H1 as [H1 H2].
rewrite (A03 B a) in H2.
specialize (H2 A).
apply H2 in H1.
assumption.
Qed.
Lemma LO9 : forall (A B C E:particular), ((forall D, D ε C
-> B ε D) /\ (A ε C /\ E ε C)) -> A ε E.
Proof.
intros A B C E.
intros H1.
destruct H1 as [H1 H2].
destruct H2 as [H2 H3].
apply (Tpart2 A C E).
- assumption.
- apply Tpart1 in H3.
assumption.
Qed.
Lemma LO10 : forall (A C :particular), (A ε C /\ (forall D, D
ε C -> D ε A)) -> C ε A.
Proof.
intros A C H1.
destruct H1 as [H1 H2].
apply Tpart1 in H1.
assumption.
Qed.
Lemma LO14 : forall (A:particular)(a:plural), A ε a -> A ε
A.
Proof.
intros A a H.
apply A01.
Qed.
Lemma LO15 : forall (A:particular), (exists (a:plural), A ε
a) <-> A ε A.
Proof.
intro A.
split.
+ intro H.
apply A01.
+ intro H.
apply A04 in H.
assumption.
Qed.
Lemma LO16 : forall (A:particular)(a:plural), A ε a ->
exists B:particular, (A ε B /\ B ε a).
Proof.
intros A a H1.
exists A.
split.
+ apply A01.
+ trivial.
Qed.
Lemma LO24 : forall (A:particular)(b:plural), A ε b ->
forall a, (A ε a \/ ~(A ε a)).
Proof.
intros A b H a.
apply classic.
Qed.
Lemma LO28 : forall (A:particular)(a:plural), A ε a <->
~~(A ε a).
Proof.
intros A a.
split.
+ intro H.
red.
intro H'.
contradiction.
+ intro H.
apply NNPP in H.
assumption.
Qed.
(* =========================== plural equality
==================================== *)
Definition Ext_Eq (a b:plural) := forall A, A ε a <-> A
ε b.
Theorem Ext_Eq_rect : forall (A :particular)(a:plural), A ε a
-> forall B:particular, A ε B -> B ε a.
Proof.
intros A a H1.
intros B H2.
rewrite (A03 A a) in H1.
specialize (H1 B).
apply (Tpart1 B A) in H2.
apply H1 in H2;assumption.
Qed.
Lemma Ext_Eq_dec : forall (x y : plural), Ext_Eq x y \/
~(Ext_Eq x y).
Proof.
intros x y.
apply classic.
Qed.
(* ================================ MEREOLOGY
==================================*)
(* element et part sous-type des pluraux *)
Class part:Type@{Name} := mkPart { pt01 : particular }.
Variable c03 : part -> plural. Coercion c03 : part
>-> plural.
Axiom TransitivePart : forall (s1:particular)(p2 p3:part), s1
ε p2 -> (@pt01 p2) ε p3 -> s1 ε p3.
Axiom AsymetricPart : forall (pA pB :part), (@pt01 pA) ε pB
-> ~((@pt01 pB) ε pA).
Class el :Type@{Name} := mkEl { el01 : particular }.
Variable c04 : el -> plural. Coercion c04 : el >->
plural.
Axiom isElement : forall (elB:el)(A :particular), A ε elB
<-> Eq_name A (@el01 elB) \/ forall ptB:part, Eq_name
(@el01 elB)(@pt01 ptB) /\ A ε ptB.
Class klass : Type@{Name} := mkKlass {
k01 : name;
k02 : exists B:particular, B ε k01 }.
(* Klass sous-type des particulars *)
Variable c07 : klass -> particular. Coercion c07 : klass
>-> particular.
Axiom isKlass : forall (elA:el)(ka:klass), (@el01 elA) ε ka
<-> (forall B, B ε (@k01 ka) -> B ε elA) /\
(forall
(elB:el), (@el01 elB) ε elA -> exists (elC elD:el), ((@el01
elC) ε (@k01 ka) /\ (@el01 elD) ε elC /\ (@el01 elD) ε elB)).
(* if plurals are identical then there is only one class *)
Lemma uniq_class : forall (cA cB:klass), Eq_name (@k01 cA)
(@k01 cB) -> Eq_name cA cB.
Proof.
destruct cA as [a p1], cB as [b p2].
simpl.
intro H.
revert p1 p2.
rewrite <-H.
intros p1 p2.
now rewrite (proof_irrelevance _ p1 p2).
Qed.
Lemma Th5 : forall (A:particular)(ptA:part), Eq_name A (@pt01
ptA) -> ~(A ε ptA).
Proof.
intros A ptA H.
red.
intro H'.
rewrite H in H'. --> fail
(*
assert (H1:=H').
apply (AsymetricPart ptA ptA) in H1.
contradiction.
*)
End
Mereo.
Le 05/12/2018 à 02:41, Fabian Kunze a
écrit :
The minimal example does not compile for me (I
assume you leave something out at "..."? ). I would have had a
look at it if it would compile.
--
Richard Dapoigny
Associate Professor - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/
