Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

V2.0 #25

Closed
wants to merge 88 commits into from
Closed

V2.0 #25

Changes from 1 commit
Commits
Show all changes
88 commits
Select commit Hold shift + click to select a range
9c49b87
blah
aleksnanevski Aug 1, 2024
b94f334
adding files
aleksnanevski Aug 1, 2024
c4ba78e
renaming
aleksnanevski Aug 1, 2024
d0cf277
blah
aleksnanevski Aug 1, 2024
fd96996
removed interlude.v
aleksnanevski Aug 1, 2024
b4d3053
started refactoring model.v
aleksnanevski Aug 1, 2024
daf3122
minor
aleksnanevski Aug 1, 2024
5af6420
started refactoring examples
aleksnanevski Aug 2, 2024
cd47cf2
continuing refactoring
aleksnanevski Aug 2, 2024
5270a21
refactored a bunch of examples.
aleksnanevski Aug 5, 2024
23ce5ab
started refactoring graph.v
aleksnanevski Aug 5, 2024
2632e78
minor
aleksnanevski Aug 5, 2024
7c38ffa
wip
aleksnanevski Aug 5, 2024
35b30ff
continuing with refactoring graph.v.
aleksnanevski Aug 6, 2024
3c21f95
blah
aleksnanevski Aug 7, 2024
1058fcf
blah
aleksnanevski Aug 7, 2024
2394b9f
blah
aleksnanevski Aug 7, 2024
79baaaf
comments about do we want to follow dangling edges to their
aleksnanevski Aug 7, 2024
a99d04d
comments
aleksnanevski Aug 7, 2024
ecdc4de
minor
aleksnanevski Aug 7, 2024
d24ddf0
minor
aleksnanevski Aug 7, 2024
443bd2e
blah
aleksnanevski Aug 8, 2024
f9a4eb5
wip
aleksnanevski Aug 8, 2024
8944fd1
wip
aleksnanevski Aug 8, 2024
83aa06d
refactored schorr.v
aleksnanevski Aug 9, 2024
7eb1ccf
committed schorr
aleksnanevski Aug 9, 2024
bcd4158
minor
aleksnanevski Aug 9, 2024
75722a2
minor
aleksnanevski Aug 9, 2024
6b3c09d
minor
aleksnanevski Aug 9, 2024
40ef923
minor
aleksnanevski Aug 9, 2024
e0c6c22
moved some helper lemmas to seqext.v
aleksnanevski Aug 9, 2024
6ef5717
blah
aleksnanevski Aug 9, 2024
f030b03
blah
aleksnanevski Aug 12, 2024
cc242ca
Merge branch 'master' of gitlab.software.imdea.org:aleks/hoare-type-t…
aleksnanevski Aug 12, 2024
ab837f6
blah
aleksnanevski Aug 12, 2024
4db8d48
blah
aleksnanevski Aug 12, 2024
3cc4ffa
blah
aleksnanevski Aug 12, 2024
e666696
blah
aleksnanevski Aug 12, 2024
b7bb9b9
blah
aleksnanevski Aug 12, 2024
bb322d1
blah
aleksnanevski Aug 12, 2024
f1e7cfe
wip
aleksnanevski Aug 12, 2024
507f228
some cleaning up in congprog.v
aleksnanevski Aug 13, 2024
67088c5
cleanup in congprog.v
aleksnanevski Aug 13, 2024
39d7b49
cleanup
aleksnanevski Aug 13, 2024
cc4be98
cleanup
aleksnanevski Aug 13, 2024
db551c3
blah
aleksnanevski Aug 13, 2024
2ff85e2
ported proofs of congr_prog
aleksnanevski Aug 14, 2024
55dfc75
modified congprog to use postconditions with vfun.
aleksnanevski Aug 14, 2024
cd96ba5
abstracting the code in congprog.v
aleksnanevski Aug 14, 2024
241fac7
defining shape predicate
Aug 14, 2024
91b6437
wMerge branch 'kevin' of https://gitlab.software.imdea.org/aleks/hoar…
Aug 14, 2024
230f0f7
made abstract type of root pointers of arrays and kvmaps be small
aleksnanevski Aug 14, 2024
5616c43
developed a number of lemmas about star.
aleksnanevski Aug 14, 2024
ab0b85c
defining shape predicate
Aug 15, 2024
642f9e0
Merge branch 'master' of https://gitlab.software.imdea.org/aleks/hoar…
Aug 15, 2024
295c20d
defining shape predicate
Aug 15, 2024
4a62478
blah
aleksnanevski Aug 15, 2024
4f64d25
reorgainzation of pred.v prelude.v and consequences.
aleksnanevski Aug 16, 2024
6798fbf
Merge branch 'master' of gitlab.software.imdea.org:aleks/hoare-type-t…
aleksnanevski Aug 16, 2024
0084f0a
removed some files that shouldn't be here
aleksnanevski Aug 16, 2024
323ccb9
moved additional lemmas from individual files to fcsl-pcm.
aleksnanevski Aug 16, 2024
77b76dc
minor
aleksnanevski Aug 16, 2024
6b9d585
sectioning of congmath.v
aleksnanevski Aug 16, 2024
50909d9
minor
aleksnanevski Aug 16, 2024
c7725aa
modifying comments
aleksnanevski Aug 16, 2024
fad9a80
changed natmap to add view for last_val
aleksnanevski Aug 27, 2024
4fd5dc9
hm
aleksnanevski Aug 27, 2024
4984d6d
removed extraneous lemmas from unionmap.v
aleksnanevski Aug 27, 2024
74ad918
minor
aleksnanevski Aug 27, 2024
7ac8e43
changed In_dom_umfilt lemma to use exists2 instead of exists.
aleksnanevski Aug 28, 2024
75bfd6b
found a way to view "weird" lemmas in natmap.v as non-weird.
aleksnanevski Aug 28, 2024
f01615c
propagating changed to natmap.v from mathador
aleksnanevski Aug 28, 2024
b426ffe
added alternative lemma for seq_lt irreflexivity, one that isn't
aleksnanevski Aug 29, 2024
af748a8
renaming slt_irrN into sltnn
aleksnanevski Aug 29, 2024
ef24ddc
added validPt2 and domPt2
aleksnanevski Aug 29, 2024
ebdc17c
propagating changes from mathador
aleksnanevski Sep 4, 2024
bea4570
blah
aleksnanevski Sep 4, 2024
93cd997
ibalh
aleksnanevski Sep 4, 2024
a45938b
blah
aleksnanevski Sep 5, 2024
1c9b614
blah
aleksnanevski Sep 5, 2024
a2283a8
blah
aleksnanevski Sep 5, 2024
48f54a2
many changes introduced to deal with graphs
aleksnanevski Sep 6, 2024
73ab034
preparing for release
aleksnanevski Sep 17, 2024
cbd2c96
removed files inheritted from fcsl-pcm
aleksnanevski Sep 23, 2024
0c83825
added Marcos to the list of authors
aleksnanevski Sep 23, 2024
ae6f24f
regenerated .opam files from meta.yml
aleksnanevski Sep 23, 2024
7ecce21
removed devcomments
aleksnanevski Sep 23, 2024
5113278
removed some lemmas that have recently been included into mathcomp
aleksnanevski Sep 23, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
blah
  • Loading branch information
aleksnanevski committed Aug 12, 2024
commit b7bb9b9c722e20bf1882959d6fe1609d99f38ee6
36 changes: 18 additions & 18 deletions core/pred.v
Original file line number Diff line number Diff line change
@@ -122,9 +122,9 @@ Arguments Pred0 {T}.
Arguments PredT {T}.
Prenex Implicits Pred0 PredT PredI PredU PredC PredD Preim.

Notation "r1 +p r2" := (PredU r1 r2 : Pred _)
Notation "r1 \+p r2" := (PredU r1 r2 : Pred _)
(at level 55, right associativity) : rel_scope.
Notation "r1 *p r2" := (xPredI r1 r2 : Pred _)
Notation "r1 \*p r2" := (xPredI r1 r2 : Pred _)
(at level 45, right associativity) : rel_scope.

Notation "[ 'Pred' : T | E ]" := (SimplPred (fun _ : T => E))
@@ -517,37 +517,37 @@ Section RelLaws.
Variable T : Type.
Implicit Type r : Pred T.

Lemma orrI r : r +p r <~> r.
Lemma orrI r : r \+p r <~> r.
Proof. by move=>x; split; [case | left]. Qed.

Lemma orrC r1 r2 : r1 +p r2 <~> r2 +p r1.
Lemma orrC r1 r2 : r1 \+p r2 <~> r2 \+p r1.
Proof. move=>x; split=>/=; tauto. Qed.

Lemma orr0 r : r +p Pred0 <~> r.
Lemma orr0 r : r \+p Pred0 <~> r.
Proof. by move=>x; split; [case | left]. Qed.

Lemma or0r r : Pred0 +p r <~> r.
Lemma or0r r : Pred0 \+p r <~> r.
Proof. by rewrite orrC orr0. Qed.

Lemma orrCA r1 r2 r3 : r1 +p r2 +p r3 <~> r2 +p r1 +p r3.
Lemma orrCA r1 r2 r3 : r1 \+p r2 \+p r3 <~> r2 \+p r1 \+p r3.
Proof. by move=>x; split=>/=; intuition. Qed.

Lemma orrAC r1 r2 r3 : (r1 +p r2) +p r3 <~> (r1 +p r3) +p r2.
Lemma orrAC r1 r2 r3 : (r1 \+p r2) \+p r3 <~> (r1 \+p r3) \+p r2.
Proof. by move=>?; split=>/=; intuition. Qed.

Lemma orrA r1 r2 r3 : (r1 +p r2) +p r3 <~> r1 +p r2 +p r3.
Lemma orrA r1 r2 r3 : (r1 \+p r2) \+p r3 <~> r1 \+p r2 \+p r3.
Proof. by rewrite (orrC r2) orrCA orrC. Qed.

(* absorption *)
Lemma orrAb r1 r2 : r1 <~> r1 +p r2 <-> r2 ~> r1.
Lemma orrAb r1 r2 : r1 <~> r1 \+p r2 <-> r2 ~> r1.
Proof.
split; first by move=>-> x /=; auto.
move=>H x /=; split; first by auto.
by case=>//; move/H.
Qed.

Lemma sub_orl r1 r2 : r1 ~> r1 +p r2. Proof. by left. Qed.
Lemma sub_orr r1 r2 : r2 ~> r1 +p r2. Proof. by right. Qed.
Lemma sub_orl r1 r2 : r1 ~> r1 \+p r2. Proof. by left. Qed.
Lemma sub_orr r1 r2 : r2 ~> r1 \+p r2. Proof. by right. Qed.
End RelLaws.

Section SubMemLaws.
@@ -563,28 +563,28 @@ Proof. by move=>H1 H2 x; split; [move/H1 | move/H2]. Qed.
Lemma subp_trans p2 p1 p3 : p1 <=p p2 -> p2 <=p p3 -> p1 <=p p3.
Proof. by move=>H1 H2 x; move/H1; move/H2. Qed.

Lemma subp_or p1 p2 q : p1 <=p q /\ p2 <=p q <-> p1 +p p2 <=p q.
Lemma subp_or p1 p2 q : p1 <=p q /\ p2 <=p q <-> p1 \+p p2 <=p q.
Proof.
split=>[[H1] H2 x|H1]; first by case; [move/H1 | move/H2].
by split=>x H2; apply: H1; [left | right].
Qed.

Lemma subp_and p1 p2 q : q <=p p1 /\ q <=p p2 <-> q <=p p1 *p p2.
Lemma subp_and p1 p2 q : q <=p p1 /\ q <=p p2 <-> q <=p p1 \*p p2.
Proof.
split=>[[H1] H2 x|] H; last by split=>x; case/H.
by split; [apply: H1 | apply: H2].
Qed.

Lemma subp_orl p1 p2 q : p1 <=p p2 -> p1 +p q <=p p2 +p q.
Lemma subp_orl p1 p2 q : p1 <=p p2 -> p1 \+p q <=p p2 \+p q.
Proof. by move=>H x; case; [move/H; left|right]. Qed.

Lemma subp_orr p1 p2 q : p1 <=p p2 -> q +p p1 <=p q +p p2.
Lemma subp_orr p1 p2 q : p1 <=p p2 -> q \+p p1 <=p q \+p p2.
Proof. by move=>H x; case; [left | move/H; right]. Qed.

Lemma subp_andl p1 p2 q : p1 <=p p2 -> p1 *p q <=p p2 *p q.
Lemma subp_andl p1 p2 q : p1 <=p p2 -> p1 \*p q <=p p2 \*p q.
Proof. by by move=>H x [H1 H2]; split; [apply: H|]. Qed.

Lemma subp_andr p1 p2 q : p1 <=p p2 -> q *p p1 <=p q *p p2.
Lemma subp_andr p1 p2 q : p1 <=p p2 -> q \*p p1 <=p q \*p p2.
Proof. by move=>H x [H1 H2]; split; [|apply: H]. Qed.

End SubMemLaws.
4 changes: 0 additions & 4 deletions examples/bst.v
Original file line number Diff line number Diff line change
@@ -17,10 +17,6 @@ From pcm Require Import options axioms pred ordtype seqext.
From pcm Require Import pcm unionmap heap autopcm automap.
From htt Require Import options model heapauto bintree.

(* hack to avoid "_ *p _" notation clash *)
From mathcomp Require order.
Import order.Order.NatOrder order.Order.TTheory.

Section BST.
Context {T : ordType}.

84 changes: 42 additions & 42 deletions examples/congmath.v
Original file line number Diff line number Diff line change
@@ -229,7 +229,7 @@ Add Morphism closure with
Proof. by apply: closE. Qed.

Lemma clos_clos (R Q : rel_exp) :
closure (closure R +p Q) <~> closure (R +p Q).
closure (closure R \+p Q) <~> closure (R \+p Q).
Proof.
case=>e1 e2; split=>H1 C H2 H3; apply: H1 =>// [[x y]] H4.
- by case: H4=>H4; [apply: H4=>// [[x1 y1]] H4|]; apply: H2; [left | right].
@@ -243,44 +243,44 @@ Proof. by rewrite -(orr0 (closure R)) clos_clos !orr0. Qed.

Lemma closKR (R1 R2 K : rel_exp) :
closure R1 <~> closure R2 ->
closure (K +p R1) <~> closure (K +p R2).
closure (K \+p R1) <~> closure (K \+p R2).
Proof.
move=>H.
by rewrite 2!(orrC K) -(clos_clos R1) -(clos_clos R2) H.
Qed.

Lemma closRK (R1 R2 K : rel_exp) :
closure R1 <~> closure R2 ->
closure (R1 +p K) <~> closure (R2 +p K).
closure (R1 \+p K) <~> closure (R2 \+p K).
Proof. by rewrite 2!(orrC _ K); apply: closKR. Qed.

Lemma closI (R : rel_exp) : R ~> closure R.
Proof. by move=>[x y] H1 T H2 H3; apply: H2. Qed.

(* absorption and closure *)
Lemma closKA (K R : rel_exp) :
closure R <~> closure (K +p R) <-> K ~> closure R.
closure R <~> closure (K \+p R) <-> K ~> closure R.
Proof.
rewrite -orrAb; split=>[->|].
- by rewrite orrAb; move=>[x y] H; apply: closI; left.
by rewrite (orrC _ R) -clos_clos orrC=><-; rewrite clos_idemp.
Qed.

Lemma closAK (K R : rel_exp) :
closure R <~> closure (R +p K) <-> K ~> closure R.
closure R <~> closure (R \+p K) <-> K ~> closure R.
Proof. by rewrite orrC closKA. Qed.

Lemma clos_or (R1 R2 R : rel_exp) :
closure R1 ~> closure R -> closure R2 ~> closure R ->
closure (R1 +p R2) ~> closure R.
closure (R1 \+p R2) ~> closure R.
Proof.
rewrite -!closAK !(orrC R) !clos_clos -!(orrC R) => H1 H2.
by rewrite H1 -clos_clos H2 clos_clos orrAC orrA.
Qed.

Lemma sub_closKR (R1 R2 K : rel_exp) :
(closure R1 ~> closure R2) ->
closure (K +p R1) ~> closure (K +p R2).
closure (K \+p R1) ~> closure (K \+p R2).
Proof.
rewrite -!closAK=>H.
rewrite -(orrC (closure _)) clos_clos orrAC -orrA orrI.
@@ -291,7 +291,7 @@ Qed.

Lemma sub_closRK (R1 R2 K : rel_exp) :
(closure R1 ~> closure R2) ->
closure (R1 +p K) ~> closure (R2 +p K).
closure (R1 \+p K) ~> closure (R2 \+p K).
Proof. by move=>H; rewrite -!(orrC K); apply: sub_closKR. Qed.

Lemma sub_closI (R1 R2 : rel_exp) :
@@ -340,7 +340,7 @@ Definition eq2rel (eq : Eq) : rel_exp :=
end.

Fixpoint eqs2rel (eqs : seq Eq) : rel_exp :=
if eqs is hd::tl then eq2rel hd +p eqs2rel tl else Pred0.
if eqs is hd::tl then eq2rel hd \+p eqs2rel tl else Pred0.

(* Coercing triples of symbols into equations *)
Definition symb2eq (t : symb*symb*symb) :=
@@ -441,7 +441,7 @@ Hint Resolve rep_in_reps : core.
(* The symbols and their representatives are a base case in defining the closure *)
Definition rep2rel D := graph (fun x => const (rep D x)).

Lemma clos_rep D R a : (const a, const (rep D a)) \In closure (rep2rel D +p R).
Lemma clos_rep D R a : (const a, const (rep D a)) \In closure (rep2rel D \+p R).
Proof.
apply: (@closI _ (const a, const (rep D a))); apply: sub_orl; rewrite /= /rep2rel /graph /=.
by rewrite mem_map /= ?mem_enum // => x1 x2 [->].
@@ -471,16 +471,16 @@ by exists a, b, c, c1, c2.
Qed.

(* The relation defined by the data structure is the following *)
Definition CRel D := closure (rep2rel D +p
lookup_rel D +p
Definition CRel D := closure (rep2rel D \+p
lookup_rel D \+p
eqs2rel (map pend2eq (pending D))).

Lemma cong_rel D : congruence (CRel D).
Proof. by move=>*; apply: cong_clos. Qed.

Hint Resolve cong_rel : core.

Lemma clos_rel D R a : (const a, const (rep D a)) \In closure (CRel D +p R).
Lemma clos_rel D R a : (const a, const (rep D a)) \In closure (CRel D \+p R).
Proof. by rewrite /CRel clos_clos orrA; apply: clos_rep. Qed.


@@ -706,12 +706,12 @@ Definition lookup_inv D :=
(* two symbols are similar if they are either related by representatives *)
(* or are to be related after the pending list is processed *)
Definition similar D a b :=
(const a, const b) \In closure (rep2rel D +p eqs2rel
(const a, const b) \In closure (rep2rel D \+p eqs2rel
(map pend2eq (pending D))).

Definition similar1 D a' b' a b :=
(const a, const b) \In
closure (rep2rel D +p [Pred x y | x = const a' /\ y = const b'] +p
closure (rep2rel D \+p [Pred x y | x = const a' /\ y = const b'] \+p
eqs2rel (map pend2eq (pending D))).

(* invariants tying use lists with the lookup table *)
@@ -830,9 +830,9 @@ Lemma symR R x y : (x, y) \In closure R <-> (y, x) \In closure R.
Proof. by split=>T; apply: symC. Qed.

Lemma app_rep D R a b x :
(x, app (const a) (const b)) \In closure (rep2rel D +p R) <->
(x, app (const a) (const b)) \In closure (rep2rel D \+p R) <->
(x, app (const (rep D a)) (const (rep D b)))
\In closure (rep2rel D +p R).
\In closure (rep2rel D \+p R).
Proof.
split=>T.
- apply: (transC (y:= app (const a) (const (rep D b)))); last first.
@@ -846,18 +846,18 @@ by apply: monoC; [apply: symC; apply: clos_rep | apply: reflC].
Qed.

Lemma app_rel D R a b x :
(x, app (const a) (const b)) \In closure (CRel D +p R) <->
(x, app (const (rep D a)) (const (rep D b))) \In closure (CRel D +p R).
(x, app (const a) (const b)) \In closure (CRel D \+p R) <->
(x, app (const (rep D a)) (const (rep D b))) \In closure (CRel D \+p R).
Proof. by rewrite /CRel !clos_clos !orrA; apply: app_rep. Qed.

Lemma const_rep D R a x :
(const a, x) \In closure (rep2rel D +p R) <->
(const (rep D a), x) \In closure (rep2rel D +p R).
(const a, x) \In closure (rep2rel D \+p R) <->
(const (rep D a), x) \In closure (rep2rel D \+p R).
Proof. by split=>T; apply: transC T; [apply: symC|]; apply: clos_rep. Qed.

Lemma const_rel D R a x :
(const a, x) \In closure (CRel D +p R) <->
(const (rep D a), x) \In closure (CRel D +p R).
(const a, x) \In closure (CRel D \+p R) <->
(const (rep D a), x) \In closure (CRel D \+p R).
Proof. by rewrite /CRel !clos_clos !orrA; apply: const_rep. Qed.

(* Now the lemmas *)
@@ -888,7 +888,7 @@ Qed.
Lemma join_class_repE (D : data) (a' b' : symb) :
a' \in reps D -> b' \in reps D -> rep_idemp D ->
closure (rep2rel (join_class D a' b')) <~>
closure (rep2rel D +p [Pred x y | x = const a' /\ y = const b']).
closure (rep2rel D \+p [Pred x y | x = const a' /\ y = const b']).
Proof.
move=>H2 H3 H1 [x y]; split=>/= T.
- pose ty z := PredU (rep2rel D) [Pred x0 y0 | x0 = const z /\ y0 = const b'].
@@ -1036,14 +1036,14 @@ Lemma join_classE (D : data) (a' b' : symb) :
rep_idemp D ->
use_lookup_inv1 D a' b' ->
lookup_use_inv1 D a' b' ->
closure (CRel (join_class D a' b') +p
closure (CRel (join_class D a' b') \+p
eqs2rel (map symb2eq (use D a'))) <~>
closure (CRel D +p [Pred x y | x = const a' /\ y = const b']).
closure (CRel D \+p [Pred x y | x = const a' /\ y = const b']).
Proof.
pose ty := [Pred x0 y0 | x0 = const a' /\ y0 = const b'].
move=>L1 L2 L3 H1 H4 H5 [x y]; split.
- apply: clos_or; move=>{x y}[x y]; last first.
- move: (clos_idemp (CRel D +p ty) (x,y))=><-.
- move: (clos_idemp (CRel D \+p ty) (x,y))=><-.
apply: sub_closI=>{x y}[[x y]] /=.
move/invert=>[c][c1][c2][->->H6].
move: (H4 a' c c1 c2 L1 H6)=>[d][d1][d2][Q1][Q2][Q3] Q4.
@@ -1194,23 +1194,23 @@ Lemma join_usePE (D : data) (a' b' : symb) :
lookup_inv (join_use D a' b') /\
use_lookup_inv2 (join_use D a' b') a' b' /\
lookup_use_inv2 (join_use D a' b') a' b' /\
closure (CRel D +p eqs2rel (map symb2eq (use D a'))) <~>
closure (CRel D \+p eqs2rel (map symb2eq (use D a'))) <~>
CRel (join_use D a' b').
Proof.
rewrite /join_use; move E: (use _ _)=>x.
elim: x D E=>[|[[c c1] c2] ss IH] D E L1 L2 H1 H2 H3 H4 H5 /=.
- by rewrite orr0 /CRel clos_idemp.
case F: (fnd _ _)=>[[[d d1] d2]|]; set D' := Data _ _ _ _ _.
- have S1: closure (rep2rel D' +p eqs2rel (map pend2eq (pending D'))) <~>
closure (rep2rel D +p [Pred x y | x = const c /\ y = const d] +p
- have S1: closure (rep2rel D' \+p eqs2rel (map pend2eq (pending D'))) <~>
closure (rep2rel D \+p [Pred x y | x = const c /\ y = const d] \+p
eqs2rel (map pend2eq (pending D))) by [].
have S2: forall e1 e2, similar D e1 e2 -> similar D' e1 e2.
- rewrite /similar=>e1 e2; move: (const e1) (const e2)=>{e1 e2} x y.
by rewrite S1; apply: sub_closI=>{x y} [[x y]];
case; [left | right; right].
have T2 : closure (CRel D' +p eqs2rel (map symb2eq ss)) <~>
closure (CRel D +p [Pred x y | x = const c /\
y = app (const c1) (const c2)] +p eqs2rel (map symb2eq ss)).
have T2 : closure (CRel D' \+p eqs2rel (map symb2eq ss)) <~>
closure (CRel D \+p [Pred x y | x = const c /\
y = app (const c1) (const c2)] \+p eqs2rel (map symb2eq ss)).
- rewrite /CRel {2 3}/D' /= !clos_clos !orrA.
rewrite -!(rpull (eqs2rel (map pend2eq _))).
rewrite -!(rpull (eqs2rel (map symb2eq ss))).
@@ -1280,7 +1280,7 @@ case F: (fnd _ _)=>[[[d d1] d2]|]; set D' := Data _ _ _ _ _.
by case: eqP H6 L1=>[->-> //| _] H6 L1; do !split=>//; apply: S2.
exists h, h1, h2; rewrite {1}/D' /= !ffunE.
by case: eqP H7 L1=>[->-> //| _] H7 L1; do !split=>//; apply: S2.
have T1: lookup_rel D' <~> lookup_rel D +p
have T1: lookup_rel D' <~> lookup_rel D \+p
[Pred x y | x = app (const (rep D c1)) (const (rep D c2)) /\
y = const (rep D c)].
- rewrite /lookup_rel /D' /= /reps /= =>[[x y]]; split.
@@ -1298,9 +1298,9 @@ have T1: lookup_rel D' <~> lookup_rel D +p
exists (rep D c1), (rep D c2), c, c1, c2.
rewrite fnd_ins !rep_in_reps.
by case: eqP.
have T2: closure (CRel D' +p eqs2rel (map symb2eq ss)) <~>
closure (CRel D +p [Pred x y | x = const c /\
y = app (const c1) (const c2)] +p eqs2rel (map symb2eq ss)).
have T2: closure (CRel D' \+p eqs2rel (map symb2eq ss)) <~>
closure (CRel D \+p [Pred x y | x = const c /\
y = app (const c1) (const c2)] \+p eqs2rel (map symb2eq ss)).
- pose ty1 := [Pred x y | x = app (const (rep D c1))
(const (rep D c2)) /\ y = const (rep D c)].
pose ty2 := [Pred x y | x = const c /\ y = app (const c1) (const c2)].
@@ -1447,8 +1447,8 @@ Proof.
move: D.
pose ty x0 y0 := [Pred x y | x = @const s x0 /\ y = @const s y0].
have L: forall D a b,
closure (rep2rel D +p ty a b) <~>
closure (rep2rel D +p ty (rep D a) (rep D b)).
closure (rep2rel D \+p ty a b) <~>
closure (rep2rel D \+p ty (rep D a) (rep D b)).
- move=>D a b [x y]; split=>T; rewrite toPredE -clos_idemp;
apply: sub_closI T=>{x y} [[x y]];
(case; first by move=>H; apply: closI; left); case=>->->;
@@ -1500,7 +1500,7 @@ have L2: forall D pend_eq p' a b a' b' D' D'',
CRel D <~> CRel (propagate (join_use D'' a' b')).
- move=>D pend_eq p' a b a' b' D' D'' H1 H H2 H3 H4 H5 H6 IH
[H7][H8][H9][H10] H11.
have T: CRel D <~> closure (CRel D' +p
have T: CRel D <~> closure (CRel D' \+p
[Pred x y | x = const a' /\ y = const b']).
- rewrite /CRel H1 -{2 3}H4 /= clos_clos !orrA H /=.
rewrite -!(rpull (lookup_rel _)) -!(rpull (eqs2rel (map pend2eq _))).
@@ -1597,7 +1597,7 @@ Lemma propagate_clos_pendP d c c1 c2 e e1 e2 :
fnd (rep d c1, rep d c2) (lookup d) = Some (e, e1, e2) ->
CRel (Data (rep d) (class d) (use d) (lookup d)
(comp_pend (c, c1, c2) (e, e1, e2) :: pending d))
<~> closure (CRel d +p
<~> closure (CRel d \+p
[Pred x y | x = const c /\ y = app (const c1) (const c2)]).
Proof.
move=>PI H.
@@ -1687,7 +1687,7 @@ Lemma propagate_clos_nopendP :
CRel (Data (rep d) (class d) u2'
(ins (rep d c1, rep d c2) (c, c1, c2) (lookup d))
(pending d)) <~>
closure (CRel d +p
closure (CRel d \+p
[Pred x y | x = const c /\ y = app (const c1) (const c2)]).
Proof.
rewrite /CRel clos_clos orrA orrAC -!orrA; apply: closRK; rewrite !orrA.