Discussion:
Rewriting through coercions
richard Dapoigny
2018-12-03 19:44:01 UTC
Hi,

I have some question about rewriting while some coercions have been set.
Some are working, others not.

Here is a minimal fragment to assess the problem.

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.

...

Class el :Type@{Name} := mkEl { el01Â  : particular }.
VariableÂ  c04 : el -> plural. Coercion c04 : el >-> plural.

Axiom isElementÂ  : forall (elB:el)(A B:particular), A Îµ elB <-> Eq_name
B (@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.

Then in order to prove the following theorem :

Lemma Th10 : forall (A:particular)(a:plural)(klA:klass), A Îµ a ->
Eq_name A (@k01 klA) -> A Îµ klA.
Proof.
intros A a kA H H'.
rewrite isKlass.
split.
- intros B H1 el1 H2.
Â  apply (isElement el1 B A).
Â  left.
Â  symmetry.
Â  exact H2.
- intros B elA elB H2.
Â  destruct H2 as [H2 H3].
Â  destruct H3 as [H3 H4].
Â  exists elA, elB.
Â  split.
Â Â Â  + rewrite <-H'.
Â Â Â Â  rewrite H2.

===================================================================

the message is: Found no subterm matching "c02 el01" in the current goal.

with hypotheses :

A : particular
a : plural
kA : klass
H : A Îµ a
H' : Eq_name A k01
B : particular
elA, elB : el
H2 : Eq_name el01 A
H3 : B Îµ elA
H4 : Eq_name el01 B
______________________________________(1/1)
el01 Îµ A

--
*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/
Fabian Kunze
2018-12-05 01:41:49 UTC
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.
Post by richard Dapoigny
Hi,
I have some question about rewriting while some coercions have been set.
Some are working, others not.
Here is a minimal fragment to assess the problem.
Universe 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).
...
Variable c04 : el -> plural. Coercion c04 : el >-> plural.
Axiom isElement : forall (elB:el)(A B:particular), A Îµ elB <-> Eq_name B
k01 : name;
k02 : exists B:particular, B Îµ k01 }.
(* Klass sous-type des particulars *)
Variable c07 : klass -> particular. Coercion c07 : klass >-> particular.
Lemma Th10 : forall (A:particular)(a:plural)(klA:klass), A Îµ a -> Eq_name
Proof.
intros A a kA H H'.
rewrite isKlass.
split.
- intros B H1 el1 H2.
apply (isElement el1 B A).
left.
symmetry.
exact H2.
- intros B elA elB H2.
destruct H2 as [H2 H3].
destruct H3 as [H3 H4].
exists elA, elB.
split.
+ rewrite <-H'.
rewrite H2.
===================================================================
the message is: Found no subterm matching "c02 el01" in the current goal.
A : particular
a : plural
kA : klass
H : A Îµ a
H' : Eq_name A k01
B : particular
elA, elB : el
H2 : Eq_name el01 A
H3 : B Îµ elA
H4 : Eq_name el01 B
______________________________________(1/1)
el01 Îµ A
--
*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/
richard Dapoigny
2018-12-05 09:10:32 UTC
Hi Fabian,

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.

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'.
+ 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.
*)

End Mereo.
Post by Fabian Kunze
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/