%%%%%% Sets of natural numbers
%%%%%% John Boyland
%%%%%% You may freely use, modify and distribute this file without restrictions.
%%%%% This file requires the "nat.elf" signature
%{%
This signature implements sets of natural numbers.
The representation is "adequate" in that every set
has a unique representation. In other words, equality of the terms
is the same as semantic equality.
%}%
%{%
This signature was created using "map" and is not "optimally" concise.
The proofs of the theorems are more general than necessary and
use many trivial lemmas.
%}%
%{%
This file follows the same theorem naming convention as nat.elf (q.v.)
%}%
%%%%% set-help.elf
%%%%% Theorems needed to help 'set' use 'map.'
%%%%% This file is part of the set.elf signature
%%%% Theorems
%{%
What follows is a series of utterly trivial theorems
about the unit type and trivial operations on it.
These theorems are needed to satisfy the map "functor".
All of these definitions are indented one space,
which signifies to the pre-module module-system
that they are internal and should not be exported.
%}%
unit`eq : unit -> unit -> type.
unit`eq/ : unit`eq unit/ unit/.
unit`ne : unit -> unit -> type. % uninhabited
unit`eq? : unit -> unit -> bool -> type.
unit`eq?/yes : unit`eq? U U true.
unit`eq?/no : unit`ne U1 U2 -> unit`eq? U1 U2 false.
%theorem unit`false-implies-eq :
forall* {U1} {U2}
forall {F:void}
exists {E:unit`eq U1 U2}
true.
%worlds () (unit`false-implies-eq _ _).
%total { } (unit`false-implies-eq _ _).
%theorem unit`eq-reflexive :
forall {U}
exists {E:unit`eq U U}
true.
- : unit`eq-reflexive unit/ unit`eq/.
%worlds () (unit`eq-reflexive _ _).
%total { } (unit`eq-reflexive _ _).
%theorem unit`eq-symmetric :
forall* {U1} {U2}
forall {E1:unit`eq U1 U2}
exists {E2:unit`eq U2 U1}
true.
- : unit`eq-symmetric unit`eq/ unit`eq/.
%worlds () (unit`eq-symmetric _ _).
%total { } (unit`eq-symmetric _ _).
%theorem unit`eq-transitive :
forall* {U1} {U2} {U3}
forall {E12:unit`eq U1 U2} {E23:unit`eq U2 U3}
exists {E13:unit`eq U1 U3}
true.
- : unit`eq-transitive unit`eq/ unit`eq/ unit`eq/.
%worlds () (unit`eq-transitive _ _ _).
%total { } (unit`eq-transitive _ _ _).
%theorem unit`false-implies-ne :
forall* {X1} {X2}
forall {F:void}
exists {G:unit`ne X1 X2}
true.
%worlds () (unit`false-implies-ne _ _).
%total { } (unit`false-implies-ne _ _).
%theorem unit`ne-respects-eq :
forall* {X1} {X2} {Y1} {Y2}
forall {D1:unit`ne X1 X2} {E1:unit`eq X1 Y1} {E2:unit`eq X2 Y2}
exists {D2:unit`ne Y1 Y2}
true.
%worlds () (unit`ne-respects-eq _ _ _ _).
%total { } (unit`ne-respects-eq _ _ _ _).
%theorem unit`ne-anti-reflexive :
forall* {X}
forall {R:unit`ne X X}
exists {F:void}
true.
%worlds () (unit`ne-anti-reflexive _ _).
%total { } (unit`ne-anti-reflexive _ _).
%theorem unit`ne-symmetric :
forall* {X} {Y}
forall {R1:unit`ne X Y}
exists {R2:unit`ne Y X}
true.
%worlds () (unit`ne-symmetric _ _).
%total { } (unit`ne-symmetric _ _).
%theorem unit`eq-ne-implies-false :
forall* {X} {Y}
forall {D1:unit`eq X Y} {D2:unit`ne X Y}
exists {F:void}
true.
%worlds () (unit`eq-ne-implies-false _ _ _).
%total { } (unit`eq-ne-implies-false _ _ _).
%theorem unit`eq?-total* :
forall {M} {N}
exists {B} {T:unit`eq? M N B}
true.
%abbrev unit`eq?-total = unit`eq?-total* _ _ _.
- : unit`eq?-total unit`eq?/yes.
%worlds () (unit`eq?-total* _ _ _ _).
%total { } (unit`eq?-total* _ _ _ _).
%abbrev unit`leq = unit`eq.
%abbrev unit`false-implies-leq = unit`false-implies-eq.
%abbrev unit`leq-reflexive = unit`eq-reflexive.
%abbrev unit`leq-transitive = unit`eq-transitive.
%theorem unit`leq-anti-symmetric :
forall* {U1} {U2}
forall {L12:unit`leq U1 U2} {L21:unit`leq U2 U1}
exists {E:unit`eq U1 U2}
true.
- : unit`leq-anti-symmetric E _ E.
%worlds () (unit`leq-anti-symmetric _ _ _).
%total { } (unit`leq-anti-symmetric _ _ _).
unit`union : unit -> unit -> unit -> type.
unit`union/ : unit`union unit/ unit/ unit/.
%theorem unit`false-implies-union :
forall* {U1} {U2} {U3}
forall {F:void}
exists {J:unit`union U1 U2 U3}
true.
%worlds () (unit`false-implies-union _ _).
%total { } (unit`false-implies-union _ _).
%theorem unit`union-deterministic :
forall* {U1} {U2} {U3} {V1} {V2} {V3}
forall {J:unit`union U1 U2 U3} {K:unit`union V1 V2 V3}
{E1:unit`eq U1 V1} {E2:unit`eq U2 V2}
exists {E3:unit`eq U3 V3}
true.
- : unit`union-deterministic unit`union/ unit`union/ unit`eq/ unit`eq/ unit`eq/.
%worlds () (unit`union-deterministic _ _ _ _ _).
%total { } (unit`union-deterministic _ _ _ _ _).
%theorem unit`union-total* :
forall {U1} {U2}
exists {U3} {J:unit`union U1 U2 U3}
true.
- : unit`union-total* _ _ _ unit`union/.
%worlds () (unit`union-total* _ _ _ _).
%total { } (unit`union-total* _ _ _ _).
%theorem unit`union-commutative :
forall* {U1} {U2} {U3}
forall {J:unit`union U1 U2 U3}
exists {K:unit`union U2 U1 U3}
true.
- : unit`union-commutative _ unit`union/.
%worlds () (unit`union-commutative _ _).
%total { } (unit`union-commutative _ _).
%theorem unit`union-associative :
forall* {U1} {U2} {U3} {U4} {U7}
forall {J12:unit`union U1 U2 U3}
{J34:unit`union U3 U4 U7}
exists {U6} {J24:unit`union U2 U4 U6}
{J16:unit`union U1 U6 U7}
true.
- : unit`union-associative _ _ unit/ unit`union/ unit`union/.
%worlds () (unit`union-associative _ _ _ _ _).
%total { } (unit`union-associative _ _ _ _ _).
%theorem unit`union-associative* :
forall* {U1} {U2} {U3} {U4} {U6} {U7}
forall {J12:unit`union U1 U2 U3}
{J34:unit`union U3 U4 U7}
{J24:unit`union U2 U4 U6}
exists {J16:unit`union U1 U6 U7}
true.
- : unit`union-associative* _ _ _ unit`union/.
%worlds () (unit`union-associative* _ _ _ _).
%total { } (unit`union-associative* _ _ _ _).
%theorem unit`union-left-preserves-leq* :
forall* {U1} {U2} {U3} {U4} {U5}
forall {L24:unit`leq U2 U4}
{J12:unit`union U1 U2 U3} {J14:unit`union U1 U4 U5}
exists {L35:unit`leq U3 U5}
true.
- : unit`union-left-preserves-leq* _ _ _ unit`eq/.
%worlds () (unit`union-left-preserves-leq* _ _ _ _).
%total { } (unit`union-left-preserves-leq* _ _ _ _).
%theorem unit`union-preserves-leq :
forall* {U1} {U2} {U3} {V1} {V2} {V3}
forall {L1:unit`leq U1 V1} {L2:unit`leq U2 V2}
{JU:unit`union U1 U2 U3} {JV:unit`union V1 V2 V3}
exists {L3:unit`leq U3 V3}
true.
- : unit`union-preserves-leq _ _ _ _ unit`eq/.
%worlds () (unit`union-preserves-leq _ _ _ _ _).
%total { } (unit`union-preserves-leq _ _ _ _ _).
%theorem unit`union-implies-leq* :
forall* {U1} {U2} {U3}
forall {J:unit`union U1 U2 U3}
exists {L:unit`leq U1 U3}
true.
- : unit`union-implies-leq* _ unit`eq/.
%worlds () (unit`union-implies-leq* _ _).
%total { } (unit`union-implies-leq* _ _).
%theorem unit`union-implies-leq :
forall* {U1} {U2} {U3}
forall {J:unit`union U1 U2 U3}
exists {L:unit`leq U1 U3} {L2:unit`leq U2 U3}
true.
- : unit`union-implies-leq _ unit`eq/ unit`eq/.
%worlds () (unit`union-implies-leq _ _ _).
%total { } (unit`union-implies-leq _ _ _).
%theorem unit`union-is-lub :
forall* {U1} {U2} {U3} {U4}
forall {J:unit`union U1 U2 U3}
{L1:unit`leq U1 U4} {L2:unit`leq U2 U4}
exists {L3:unit`leq U3 U4}
true.
- : unit`union-is-lub _ _ _ unit`eq/.
%worlds () (unit`union-is-lub _ _ _ _).
%total { } (unit`union-is-lub _ _ _ _).
%abbrev unit`intersection = unit`union.
%abbrev unit`false-implies-intersection = unit`false-implies-union.
%abbrev unit`intersection-deterministic = unit`union-deterministic.
%abbrev unit`intersection-total* = unit`union-total*.
%abbrev unit`intersection-commutative = unit`union-commutative.
%abbrev unit`intersection-associative = unit`union-associative.
%abbrev unit`intersection-associative* = unit`union-associative*.
%abbrev unit`intersection-implies-leq* = unit`union-implies-leq*.
%abbrev unit`intersection-left-preserves-leq* = unit`union-left-preserves-leq*.
%theorem unit`intersection-is-glb :
forall* {U0} {U1} {U2} {U3}
forall {A:unit`intersection U1 U2 U3}
{L1:unit`leq U0 U1} {L2:unit`leq U0 U2}
exists {L3:unit`leq U0 U3}
true.
- : unit`intersection-is-glb _ _ _ unit`eq/.
%worlds () (unit`intersection-is-glb _ _ _ _).
%total { } (unit`intersection-is-glb _ _ _ _).
%theorem unit`intersection-right-distributes-over-union :
forall* {U1} {U2} {U3} {U4} {U7}
forall {J:unit`union U1 U2 U3} {A:unit`intersection U3 U4 U7}
exists {U5} {U6} {M14:unit`intersection U1 U4 U5} {M24:unit`intersection U2 U4 U6}
{J56:unit`union U5 U6 U7}
true.
- : unit`intersection-right-distributes-over-union _ _ unit/ unit/ unit`union/
unit`union/ unit`union/.
%worlds () (unit`intersection-right-distributes-over-union _ _ _ _ _ _ _).
%total { } (unit`intersection-right-distributes-over-union _ _ _ _ _ _ _).
%abbrev unit`union-right-distributes-over-intersection =
unit`intersection-right-distributes-over-union.
%%%% Functor Use
%%%% Definitions of Maps
map : type.
map/0 : map.
map/+ : nat -> unit -> map -> map.
%%%% Relations on maps
eq : map -> map -> type.
eq/ : eq M M.
ne : map -> map -> type.
ne/L : ne map/0 (map/+ _ _ _).
ne/R : ne (map/+ _ _ _) map/0.
ne/N : nat`ne N1 N2 -> ne (map/+ N1 _ _) (map/+ N2 _ _).
ne/D : unit`ne D1 D2 -> ne (map/+ _ D1 _) (map/+ _ D2 _).
ne/+ : ne M1 M2 -> ne (map/+ _ _ M1) (map/+ _ _ M2).
eq? : map -> map -> bool -> type.
eq?/yes : eq? X X true.
eq?/no : eq? X Y false
<- ne X Y.
lookup : map -> nat -> unit -> type.
lookup/= : lookup (map/+ N1 D _) N2 D
<- nat`eq N1 N2.
lookup/> : lookup (map/+ N1 _ F) N2 D
<- plus (s N0) N1 N2
<- lookup F N0 D.
not-member : map -> nat -> type.
not-member/0 : not-member map/0 M.
not-member/< : not-member (map/+ N _ F) M
<- gt N M.
not-member/> : not-member (map/+ N _ F) M
<- plus (s M1) N M
<- not-member F M1.
member? : map -> nat -> bool -> type.
member?/in : member? M N true
<- lookup M N _.
member?/out : member? M N false
<- not-member M N.
disjoint : map -> map -> type.
disjoint/L : disjoint map/0 M.
disjoint/R : disjoint M map/0.
disjoint/< : disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`plus (s N0) N1 N2
<- disjoint M1 (map/+ N0 D2 M2).
disjoint/> : disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`plus (s N3) N2 N1
<- disjoint (map/+ N3 D1 M1) M2.
disjoint? : map -> map -> bool -> type.
disjoint?/yes : disjoint M1 M2 -> disjoint? M1 M2 true.
disjoint?/no :
lookup M1 N D1 ->
lookup M2 N D2 ->
disjoint? M1 M2 false.
size : map -> nat -> type.
size/0 : size map/0 z.
size/+ : size (map/+ _ _ M) (s N)
<- size M N.
%% useful for proving termination on map operations:
bound : map -> nat -> type.
bound/0 : bound map/0 z.
bound/+ : bound (map/+ N1 D M) N3
<- bound M N2
<- plus (s N1) N2 N3.
shift : nat -> map -> map -> type.
shift/0 : shift _ map/0 map/0.
shift/+ : shift N1 (map/+ N2 D M) (map/+ N3 D M)
<- plus (s N1) N2 N3.
update : map -> nat -> unit -> map -> type.
update/0 : update map/0 N D (map/+ N D map/0).
update/= : update (map/+ N1 _ F) N2 D (map/+ N2 D F)
<- nat`eq N1 N2.
update/< : update (map/+ N1 D1 F) N2 D2 (map/+ N2 D2 (map/+ N3 D1 F))
<- plus (s N3) N2 N1.
update/> : update (map/+ N1 D1 F1) N2 D2 (map/+ N1 D1 F2)
<- plus (s N0) N1 N2
<- update F1 N0 D2 F2.
%%%% Theorems
%%% Theorems about eq
%theorem meta-eq :
forall {M} {N} {E:eq M N}
true.
- : meta-eq M M eq/.
%worlds () (meta-eq _ _ _).
%total {} (meta-eq _ _ _).
%reduces M = N (meta-eq M N _).
%theorem false-implies-eq :
forall* {M} {M'} forall {F:void} exists {E:eq M M'} true.
%worlds () (false-implies-eq _ %{=>}% M=M').
%total {} (false-implies-eq _ _).
%theorem eq-reflexive : forall {M} exists {E:eq M M} true.
- : eq-reflexive _ eq/.
%worlds () (eq-reflexive M %{=>}% M=M).
%total {} (eq-reflexive _ _).
%theorem eq-symmetric :
forall* {M} {M'}
forall {E1:eq M M'}
exists {E2:eq M' M}
true.
- : eq-symmetric eq/ eq/.
%worlds () (eq-symmetric M=M' %{=>}% M'=M).
%total {} (eq-symmetric _ _).
%theorem eq-transitive:
forall* {M1} {M2} {M3}
forall {E12:eq M1 M2} {E23:eq M2 M3}
exists {E13:eq M1 M3}
true.
- : eq-transitive eq/ eq/ eq/.
%worlds () (eq-transitive M1=M2 M2=M3 %{=>}% M1=M3).
%total {} (eq-transitive _ _ _).
%theorem map/+-preserves-eq :
forall* {N} {NP} {D} {DP} {F} {FP}
forall {EN:nat`eq N NP} {ED:unit`eq D DP} {EF:eq F FP}
exists {E:eq (map/+ N D F) (map/+ NP DP FP)}
true.
- : map/+-preserves-eq nat`eq/ unit`eq/ eq/ eq/.
%worlds () (map/+-preserves-eq N=N' D=D' F=F' %{=>}% NDF=N'D'F').
%total {} (map/+-preserves-eq _ _ _ _).
%theorem map/+-preserves-eq-converse :
forall* {N} {NP} {D} {DP} {F} {FP}
forall {E:eq (map/+ N D F) (map/+ NP DP FP)}
exists {EN:nat`eq N NP} {ED:unit`eq D DP} {EF:eq F FP}
true.
- : map/+-preserves-eq-converse eq/ nat`eq/ unit`eq/ eq/.
%worlds () (map/+-preserves-eq-converse _ _ _ _).
%total {} (map/+-preserves-eq-converse _ _ _ _).
%theorem eq-no-occur :
forall* {M} {N} {D}
forall {E:eq M (map/+ N D M)}
exists {F:void}
true.
%worlds () (eq-no-occur _ _).
%total {} (eq-no-occur _ _).
%theorem eq-contradiction :
forall* {N} {D} {M}
forall {E:eq map/0 (map/+ N D M)}
exists {F:void}
true.
%worlds () (eq-contradiction _ _).
%total {} (eq-contradiction _ _).
%%% Theorems about ne
%theorem false-implies-ne :
forall* {M1} {M2}
forall {F:void}
exists {N:ne M1 M2}
true.
%worlds () (false-implies-ne _ _).
%total { } (false-implies-ne _ _).
%theorem ne-respects-eq :
forall* {M11} {M12} {M21} {M22}
forall {N1:ne M11 M12} {E1:eq M11 M21} {E2:eq M12 M22}
exists {N2:ne M21 M22}
true.
- : ne-respects-eq N eq/ eq/ N.
%worlds () (ne-respects-eq _ _ _ _).
%total { } (ne-respects-eq _ _ _ _).
%theorem ne-anti-reflexive :
forall* {M}
forall {N:ne M M}
exists {F:void}
true.
- : ne-anti-reflexive (ne/N N) F
<- nat`ne-anti-reflexive N F.
- : ne-anti-reflexive (ne/D N) F
<- unit`ne-anti-reflexive N F.
- : ne-anti-reflexive (ne/+ N) F
<- ne-anti-reflexive N F.
%worlds () (ne-anti-reflexive _ _).
%total (N) (ne-anti-reflexive N _).
%theorem ne-symmetric :
forall* {M1} {M2}
forall {N1:ne M1 M2}
exists {N2:ne M2 M1}
true.
- : ne-symmetric ne/L ne/R.
- : ne-symmetric ne/R ne/L.
- : ne-symmetric (ne/N N1) (ne/N N2)
<- nat`ne-symmetric N1 N2.
- : ne-symmetric (ne/D N1) (ne/D N2)
<- unit`ne-symmetric N1 N2.
- : ne-symmetric (ne/+ N1) (ne/+ N2)
<- ne-symmetric N1 N2.
%worlds () (ne-symmetric _ _).
%total (N) (ne-symmetric N _).
%theorem eq-ne-implies-false :
forall* {X} {Y}
forall {D1:eq X Y} {D2:ne X Y}
exists {F:void}
true.
- : eq-ne-implies-false eq/ X<>X F
<- ne-anti-reflexive X<>X F.
%worlds () (eq-ne-implies-false _ _ _).
%total { } (eq-ne-implies-false _ _ _).
%theorem eq?-total* :
forall {M} {N}
exists {B} {T:eq? M N B}
true.
%abbrev eq?-total = eq?-total* _ _ _.
%theorem eq?-total/+ :
forall* {N1} {D1} {N2} {D2} {M2} {EN} {ED} {EM}
forall {M1}
{EN?:nat`eq? N1 N2 EN}
{ED?:unit`eq? D1 D2 ED}
{EM?:eq? M1 M2 EM}
exists {B}
{E?:eq? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
- : eq?-total eq?/yes.
- : eq?-total (eq?/no ne/L).
- : eq?-total (eq?/no ne/R).
- : eq?-total E?
<- nat`eq?-total EN?
<- unit`eq?-total ED?
<- eq?-total EM?
<- eq?-total/+ _ EN? ED? EM? _ E?.
- : eq?-total/+ _ (nat`eq?/yes) (unit`eq?/yes) (eq?/yes) _ eq?/yes.
- : eq?-total/+ _ (nat`eq?/no N) _ _ _ (eq?/no (ne/N N)).
- : eq?-total/+ _ _ (unit`eq?/no N) _ _ (eq?/no (ne/D N)).
- : eq?-total/+ _ _ _ (eq?/no N) _ (eq?/no (ne/+ N)).
%worlds () (eq?-total* _ _ _ _) (eq?-total/+ _ _ _ _ _ _).
%total (M W) (eq?-total* M _ _ _) (eq?-total/+ W _ _ _ _ _).
%%% Theorems about lookup
%theorem false-implies-lookup :
forall* {M} {N} {D}
forall {F:void}
exists {L:lookup M N D}
true.
%worlds () (false-implies-lookup _ %{=>}% F^N=D).
%total {} (false-implies-lookup _ _).
%theorem lookup-respects-eq :
forall* {M} {N} {D} {MP} {NP} {DP}
forall {L:lookup M N D} {EM:eq M MP} {EN:nat`eq N NP} {ED:unit`eq D DP}
exists {LP:lookup MP NP DP}
true.
- : lookup-respects-eq L eq/ nat`eq/ unit`eq/ L.
%worlds () (lookup-respects-eq M^N=D M=M' N=N' D=D' %{=>}% M'^N'=D').
%total {} (lookup-respects-eq _ _ _ _ _).
%theorem lookup-deterministic :
forall* {M} {N} {D} {MP} {NP} {DP}
forall {L:lookup M N D} {LP:lookup MP NP DP}
{EM:eq M MP} {EN:nat`eq N NP}
exists {ED:unit`eq D DP}
true.
- : lookup-deterministic (lookup/= nat`eq/) (lookup/= nat`eq/) eq/ nat`eq/ unit`eq/.
- : lookup-deterministic (lookup/> F^N0=D N0+1+N1=N2)
(lookup/> F^N0'=D' N0'+1+N1=N2) eq/ nat`eq/ D=D'
<- plus-right-cancels N0+1+N1=N2 N0'+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0'
<- lookup-deterministic F^N0=D F^N0'=D' eq/ N0=N0' D=D'.
%% contradiction cases
- : lookup-deterministic (lookup/= nat`eq/) (lookup/> _ N0+1+N=N)
eq/ nat`eq/ D=D'
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N FALSE
<- unit`false-implies-eq FALSE D=D'.
- : lookup-deterministic (lookup/> _ N0+1+N=N) (lookup/= nat`eq/)
eq/ nat`eq/ D=D'
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N FALSE
<- unit`false-implies-eq FALSE D=D'.
%worlds () (lookup-deterministic M^N=D M'^N'=D' M=M' N=N' %{=>}% D=D').
%total (L) (lookup-deterministic L _ _ _ _).
%% lookup is NOT total
%theorem lookup-contradiction :
forall* {N} {D}
forall {L:lookup map/0 N D}
exists {F:void}
true.
%worlds () (lookup-contradiction _ _).
%total { } (lookup-contradiction _ _).
%theorem lookup-one-choice :
forall* {N1} {D1} {N2} {D2}
forall {L:lookup (map/+ N1 D1 map/0) N2 D2}
exists {NE:nat`eq N1 N2} {DE:unit`eq D1 D2}
true.
- : lookup-one-choice (lookup/= nat`eq/) nat`eq/ unit`eq/.
%worlds () (lookup-one-choice _ _ _).
%total { } (lookup-one-choice _ _ _).
%theorem lookup-ne-implies-ne :
forall* {M1} {N1} {D1} {M2} {N2} {D2}
forall {L1:lookup M1 N1 D1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
{ND:unit`ne D1 D2}
exists {NM:ne M1 M2}
true.
%theorem lookup-ne-implies-ne/L :
forall* {M1} {N1} {D1} {M2} {N2} {D2} {B}
forall {L1:lookup M1 N1 D1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
{ND:unit`ne D1 D2}
{EM?:eq? M1 M2 B}
exists {NM:ne M1 M2}
true.
- : lookup-ne-implies-ne L1 L2 EN ND NM
<- eq?-total EM?
<- lookup-ne-implies-ne/L L1 L2 EN ND EM? NM.
- : lookup-ne-implies-ne/L L1 L2 _ _ (eq?/no NM) NM.
- : lookup-ne-implies-ne/L L1 L2 nat`eq/ D1<>D2 eq?/yes NM
<- lookup-deterministic L1 L2 eq/ nat`eq/ D1=D2
<- unit`eq-ne-implies-false D1=D2 D1<>D2 F
<- false-implies-ne F NM.
%worlds () (lookup-ne-implies-ne/L _ _ _ _ _ _).
%total { } (lookup-ne-implies-ne/L _ _ _ _ _ _).
%worlds () (lookup-ne-implies-ne _ _ _ _ _).
%total { } (lookup-ne-implies-ne _ _ _ _ _).
%%% Theorems about not-member
%theorem false-implies-not-member :
forall* {M} {N} forall {F:void} exists {D:not-member M N} true.
%worlds () (false-implies-not-member _ %{=>}% N-not-in-member-M).
%total {} (false-implies-not-member _ _).
%theorem not-member-respects-eq :
forall* {M} {N} {MP} {NP}
forall {D:not-member M N} {EM:eq M MP} {EN:nat`eq N NP}
exists {DP:not-member MP NP}
true.
- : not-member-respects-eq D eq/ nat`eq/ D.
%worlds () (not-member-respects-eq _ _ _ _).
%total {} (not-member-respects-eq _ _ _ _).
%% not-member is NOT deterministic
%theorem not-member-total* :
forall {M}
exists {N} {F:not-member M N}
true.
- : not-member-total* map/0 z not-member/0.
- : not-member-total* (map/+ N1 _ M) N3 (not-member/> F N+1+N1=N3)
<- not-member-total* M N F
<- plus-total* (s N) N1 N3 N+1+N1=N3.
%worlds () (not-member-total* M %{=>}% N N-not-in-member-of-M).
%total (M) (not-member-total* M _ _).
%abbrev not-member-total = not-member-total* _ _.
%theorem not-member-lookup-not-equal :
forall* {M} {N1} {N2} {D2}
forall {F:not-member M N1} {L:lookup M N2 D2}
exists {NE:nat`ne N1 N2}
true.
- : not-member-lookup-not-equal (not-member/< N2>N1) (lookup/= nat`eq/) (nat`ne/< N2>N1).
- : not-member-lookup-not-equal (not-member/< N1>N3) (lookup/> _ N0+1+N1=N2)
(nat`ne/< N2>N3)
<- plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- gt-transitive N2>N1 N1>N3 N2>N3.
- : not-member-lookup-not-equal (not-member/> _ X+1+N2=N1) (lookup/= nat`eq/) (nat`ne/> N1>N2)
<- plus-implies-gt X+1+N2=N1 nat`eq/ N1>N2.
- : not-member-lookup-not-equal (not-member/> F N4+1+N1=N3) (lookup/> L N0+1+N1=N2)
N3<>N2
<- not-member-lookup-not-equal F L N4<>N0
<- succ-preserves-ne N4<>N0 N4+1<>N0+1
<- plus-right-preserves-ne* N4+1<>N0+1 N4+1+N1=N3 N0+1+N1=N2 N3<>N2.
%worlds () (not-member-lookup-not-equal N1-not-in-member-of-M M^N2=D %{=>}% N1<>N2).
%total (F) (not-member-lookup-not-equal F _ _).
%theorem not-member-contradiction :
forall* {M} {N} {D}
forall {F:not-member (map/+ N D M) N}
exists {V:void}
true.
- : not-member-contradiction (not-member/< N>N) V
<- nat`gt-anti-reflexive N>N V.
- : not-member-contradiction (not-member/> _ N0+1+N=N) V
<- nat`plus-implies-gt N0+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N V.
%worlds () (not-member-contradiction _ _).
%total {} (not-member-contradiction _ _).
%theorem ne-implies-unit-map-not-member :
forall* {N1} {D} {N2}
forall {NE:nat`ne N1 N2}
exists {F:not-member (map/+ N1 D map/0) N2}
true.
- : ne-implies-unit-map-not-member
(nat`ne/< N1 not-member/0 N0+1+N1=N2)
<- nat`gt-implies-plus N1 N1>N2) (not-member/< N1>N2).
%worlds () (ne-implies-unit-map-not-member _ _).
%total { } (ne-implies-unit-map-not-member _ _).
%theorem plus-right-preserves-not-member* :
forall* {M} {N1} {D} {N2} {N} {N3} {N4}
forall {F:not-member (map/+ N1 D M) N2}
{P1:plus N1 N N3} {P2:plus N2 N N4}
exists {FP:not-member (map/+ N3 D M) N4}
true.
- : plus-right-preserves-not-member* (not-member/< N2>N1) N1+N=N3 N2+N=N4 (not-member/< N4>N3)
<- nat`plus-right-preserves-gt* N2>N1 N1+N=N3 N2+N=N4 N4>N3.
- : plus-right-preserves-not-member* (not-member/> F10 N0+1+N1=N2) N1+N=N3 N2+N=N4
(not-member/> F10 N0+1+N3=N4)
<- nat`plus-associative* N0+1+N1=N2 N2+N=N4 N1+N=N3 N0+1+N3=N4.
%worlds () (plus-right-preserves-not-member* _ _ _ _).
%total {} (plus-right-preserves-not-member* _ _ _ _).
%theorem not-member-lookup-implies-ne :
forall* {M1} {N1} {M2} {N2} {D2}
forall {L1:not-member M1 N1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
exists {NM:ne M1 M2}
true.
%theorem not-member-lookup-implies-ne/L :
forall* {M1} {N1} {M2} {N2} {D2} {B}
forall {L1:not-member M1 N1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
{EM?:eq? M1 M2 B}
exists {NM:ne M1 M2}
true.
- : not-member-lookup-implies-ne F1 L2 EN NM
<- eq?-total EM?
<- not-member-lookup-implies-ne/L F1 L2 EN EM? NM.
- : not-member-lookup-implies-ne/L _ _ _ (eq?/no NM) NM.
- : not-member-lookup-implies-ne/L F1 L2 nat`eq/ eq?/yes NM
<- not-member-lookup-not-equal F1 L2 N<>N
<- nat`ne-anti-reflexive N<>N F
<- false-implies-ne F NM.
%worlds () (not-member-lookup-implies-ne/L _ _ _ _ _).
%total { } (not-member-lookup-implies-ne/L _ _ _ _ _).
%worlds () (not-member-lookup-implies-ne _ _ _ _).
%total { } (not-member-lookup-implies-ne _ _ _ _).
%%% Theorems about map/member
%theorem false-implies-member? :
forall* {M} {N} {D}
forall {F:void}
exists {MD:member? M N D}
true.
%worlds () (false-implies-member? _ _).
%total {} (false-implies-member? _ _).
%theorem member?-respects-eq :
forall* {M1} {N1} {B1} {M2} {N2} {B2}
forall {MD1:member? M1 N1 B1}
{EM:eq M1 M2}
{EN:nat`eq N1 N2}
{BE:bool`eq B1 B2}
exists {MD2:member? M2 N2 B2}
true.
- : member?-respects-eq MD eq/ nat`eq/ bool`eq/ MD.
%worlds () (member?-respects-eq _ _ _ _ _).
%total { } (member?-respects-eq _ _ _ _ _).
%theorem member?-deterministic :
forall* {M1} {N1} {B1} {M2} {N2} {B2}
forall {MD1:member? M1 N1 B1}
{MD2:member? M2 N2 B2}
{EM:eq M1 M2}
{EN:nat`eq N1 N2}
exists {BE:bool`eq B1 B2}
true.
- : member?-deterministic _ _ _ _ bool`eq/.
- : member?-deterministic (member?/in L) (member?/out F) eq/ nat`eq/ BE
<- not-member-lookup-not-equal F L NE
<- nat`ne-anti-reflexive NE V
<- bool`false-implies-eq V BE.
- : member?-deterministic (member?/out F) (member?/in L) eq/ nat`eq/ BE
<- not-member-lookup-not-equal F L NE
<- nat`ne-anti-reflexive NE V
<- bool`false-implies-eq V BE.
%worlds () (member?-deterministic _ _ _ _ _).
%total { } (member?-deterministic _ _ _ _ _).
%theorem member?-total* :
forall {M} {N}
exists {B} {MD:member? M N B}
true.
%% we need a lemma
%theorem member?-map/+-total :
forall {N1} {D1} {M1} {N2} {C} {CMP:nat`compare N1 N2 C}
exists {B} {MD:member? (map/+ N1 D1 M1) N2 B}
true.
%% and this lemma needs a lemma
%theorem member?-map/+-complete :
forall {N1} {D1} {M1} {N2} {N0} {P:plus (s N0) N1 N2}
{B} {MD1:member? M1 N0 B}
exists {MD:member? (map/+ N1 D1 M1) N2 B}
true.
- : member?-total* map/0 N false (member?/out not-member/0).
- : member?-total* (map/+ N1 D1 M1) N2 B MD
<- nat`compare-total* N1 N2 C CMP
<- member?-map/+-total N1 D1 M1 N2 C CMP B MD.
- : member?-map/+-total N1 D1 M1 N2 equal CMP true
(member?/in (lookup/= N1=N2))
<- equal-implies-eq CMP N1=N2.
- : member?-map/+-total N1 D1 M1 N2 greater CMP false
(member?/out (not-member/< N1>N2))
<- greater-implies-gt CMP N1>N2.
- : member?-map/+-total N1 D1 M1 N2 less CMP B MD
<- less-implies-lt CMP N2>N1
<- gt-implies-plus N2>N1 N0 N0+1+N1=N2
<- member?-total* M1 N0 B MD1
<- member?-map/+-complete N1 D1 M1 N2 N0 N0+1+N1=N2 B MD1 MD.
- : member?-map/+-complete N1 D1 M1 N2 N0 N0+1+N1=N2 true (member?/in L1)
(member?/in (lookup/> L1 N0+1+N1=N2)).
- : member?-map/+-complete N1 D1 M1 N2 N0 N0+1+N1=N2 false (member?/out F1)
(member?/out (not-member/> F1 N0+1+N1=N2)).
%worlds () (member?-map/+-complete _ _ _ _ _ _ _ _ _).
%total {} (member?-map/+-complete _ _ _ _ _ _ _ _ _).
%worlds () (member?-total* _ _ _ _)
(member?-map/+-total _ _ _ _ _ _ _ _).
%total (M M1) (member?-total* M _ _ _)
(member?-map/+-total _ _ M1 _ _ _ _ _).
%abbrev member?-total = member?-total* _ _ _.
%theorem in-implies-lookup :
forall* {M} {N}
forall {MD:member? M N true}
exists {D} {L:lookup M N D}
true.
- : in-implies-lookup (member?/in L) _ L.
%worlds () (in-implies-lookup _ _ _).
%total {} (in-implies-lookup _ _ _).
%theorem out-implies-not-member :
forall* {M} {N}
forall {MD:member? M N false}
exists {F:not-member M N}
true.
- : out-implies-not-member (member?/out F) F.
%worlds () (out-implies-not-member _ _).
%total {} (out-implies-not-member _ _).
%%% Theorems about disjoint
%theorem false-implies-disjoint :
forall* {M1} {M2}
forall {F:void}
exists {D:disjoint M1 M2}
true.
%worlds () (false-implies-disjoint _ _).
%total { } (false-implies-disjoint _ _).
%theorem disjoint-respects-eq :
forall* {M1} {M2} {M1P} {M2P}
forall {A:disjoint M1 M2} {E1:eq M1 M1P} {E2:eq M2 M2P}
exists {AP:disjoint M1P M2P}
true.
- : disjoint-respects-eq A eq/ eq/ A.
%worlds () (disjoint-respects-eq _ _ _ _).
%total {} (disjoint-respects-eq _ _ _ _).
%reduces A = AP (disjoint-respects-eq A _ _ AP).
%theorem disjoint/=-contradiction :
forall* {N1} {D1} {M1} {N2} {D2} {M2}
forall {A:disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{G:nat`eq N1 N2}
exists {F:void}
true.
- : disjoint/=-contradiction (disjoint/< _ N0+1+N=N) nat`eq/ F
<- nat`plus-implies-gt N0+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F.
- : disjoint/=-contradiction (disjoint/> _ N3+1+N=N) nat`eq/ F
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F.
%worlds () (disjoint/=-contradiction _ _ _).
%total { } (disjoint/=-contradiction _ _ _).
%theorem disjoint/<-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0}
forall {A:disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N0) N1 N2}
exists {AP:disjoint M1 (map/+ N0 D2 M2)}
true.
- : disjoint/<-inversion (disjoint/< A P) P' A'
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0P
<- map/+-preserves-eq N0=N0P unit`eq/ eq/ M022=M022'
<- disjoint-respects-eq A eq/ M022=M022' A'.
- : disjoint/<-inversion (disjoint/> A' N3+1+N2=N1) N0+1+N1=N2 A
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M311=M1
<- false-implies-eq F M2=M022
<- disjoint-respects-eq A' M311=M1 M2=M022 A.
%worlds () (disjoint/<-inversion _ _ _).
%total {} (disjoint/<-inversion _ _ _).
%reduces AP < A (disjoint/<-inversion A _ AP).
%theorem disjoint/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3}
forall {A:disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N3) N2 N1}
exists {AP:disjoint (map/+ N3 D1 M1) M2}
true.
- : disjoint/>-inversion (disjoint/> A P) P' A'
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N3+1=N3'+1
<- succ-cancels N3+1=N3'+1 N3=N3P
<- map/+-preserves-eq N3=N3P unit`eq/ eq/ M311=M311'
<- disjoint-respects-eq A M311=M311' eq/ A'.
- : disjoint/>-inversion (disjoint/< A' N0+1+N1=N2) N3+1+N2=N1 A
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M1=M311
<- false-implies-eq F M022=M2
<- disjoint-respects-eq A' M1=M311 M022=M2 A.
%worlds () (disjoint/>-inversion _ _ _).
%total { } (disjoint/>-inversion _ _ _).
%reduces AP < A (disjoint/>-inversion A _ AP).
%theorem disjoint-anti-reflexive :
forall* {M}
forall {D:disjoint M M}
exists {E:eq map/0 M}
true.
- : disjoint-anti-reflexive disjoint/L eq/.
- : disjoint-anti-reflexive disjoint/R eq/.
- : disjoint-anti-reflexive (A:disjoint (map/+ N D M) (map/+ N D M)) E
<- disjoint/=-contradiction A nat`eq/ F
<- false-implies-eq F E.
%worlds () (disjoint-anti-reflexive _ _).
%total { } (disjoint-anti-reflexive _ _).
%theorem disjoint-symmetric :
forall* {M1} {M2}
forall {D:disjoint M1 M2}
exists {D:disjoint M2 M1}
true.
- : disjoint-symmetric disjoint/L disjoint/R.
- : disjoint-symmetric disjoint/R disjoint/L.
- : disjoint-symmetric (disjoint/< D P) (disjoint/> D' P)
<- disjoint-symmetric D D'.
- : disjoint-symmetric (disjoint/> D P) (disjoint/< D' P)
<- disjoint-symmetric D D'.
%worlds () (disjoint-symmetric _ _).
%total (D) (disjoint-symmetric D _).
%theorem disjoint-lookup-contradiction :
forall* {M1} {M2} {N} {D1} {D2}
forall {A:disjoint M1 M2}
{L1:lookup M1 N D1} {L2:lookup M2 N D2}
exists {F:void}
true.
- : disjoint-lookup-contradiction disjoint/L L _ F
<- lookup-contradiction L F.
- : disjoint-lookup-contradiction disjoint/R _ L F
<- lookup-contradiction L F.
- : disjoint-lookup-contradiction (disjoint/< _ N0+1+N=N)
(lookup/= nat`eq/) (lookup/= nat`eq/) F
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F.
- : disjoint-lookup-contradiction (disjoint/< _ N0+1+N1=N2)
(lookup/= nat`eq/)
(lookup/> _ N3+1+N2=N1) F
<- plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- gt-anti-symmetric N2>N1 N1>N2 F.
- : disjoint-lookup-contradiction (disjoint/< D N0+1+N1=N2)
(lookup/> L1P N0P+1+N1=N2)
(lookup/= nat`eq/) F
<- plus-right-cancels N0P+1+N1=N2 N0+1+N1=N2 nat`eq/ nat`eq/ N0P+1=N0+1
<- succ-cancels N0P+1=N0+1 N0P=N0
<- lookup-respects-eq L1P eq/ N0P=N0 unit`eq/ L1
<- disjoint-lookup-contradiction D L1 (lookup/= nat`eq/) F.
- : disjoint-lookup-contradiction (disjoint/< D N0+1+N1=N2)
(lookup/> L1 N1P+1+N1=N)
(lookup/> L2 N2P+1+N2=N) F
<- plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- plus-associative-converse N0+N1+1=N2 N2P+1+N2=N NX
N2P+1+N0=NX NX+N1+1=N
<- plus-swap-succ N1P+1+N1=N N1P+N1+1=N
<- plus-right-cancels NX+N1+1=N N1P+N1+1=N nat`eq/ nat`eq/ NX=N1P
<- plus-respects-eq N2P+1+N0=NX nat`eq/ nat`eq/ NX=N1P N2P+1+N0=N1P
<- disjoint-lookup-contradiction D L1 (lookup/> L2 N2P+1+N0=N1P) F.
- : disjoint-lookup-contradiction (disjoint/> _ N3+1+N=N)
(lookup/= nat`eq/) (lookup/= nat`eq/) F
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F.
- : disjoint-lookup-contradiction (disjoint/> _ N3+1+N2=N1)
(lookup/> _ N3+1+N1=N2)
(lookup/= nat`eq/) F
<- plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- plus-implies-gt N3+1+N1=N2 nat`eq/ N2>N1
<- gt-anti-symmetric N1>N2 N2>N1 F.
- : disjoint-lookup-contradiction (disjoint/> D N3+1+N2=N1)
(lookup/= nat`eq/)
(lookup/> L2P N3P+1+N2=N1) F
<- plus-right-cancels N3P+1+N2=N1 N3+1+N2=N1 nat`eq/ nat`eq/ N3P+1=N3+1
<- succ-cancels N3P+1=N3+1 N3P=N3
<- lookup-respects-eq L2P eq/ N3P=N3 unit`eq/ L2
<- disjoint-lookup-contradiction D (lookup/= nat`eq/) L2 F.
- : disjoint-lookup-contradiction (disjoint/> D N3+1+N2=N1)
(lookup/> L1 N1P+1+N1=N)
(lookup/> L2 N2P+1+N2=N) F
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 N1P+1+N1=N NX
N1P+1+N3=NX NX+N2+1=N
<- plus-swap-succ N2P+1+N2=N N2P+N2+1=N
<- plus-right-cancels NX+N2+1=N N2P+N2+1=N nat`eq/ nat`eq/ NX=N2P
<- plus-respects-eq N1P+1+N3=NX nat`eq/ nat`eq/ NX=N2P N1P+1+N3=N2P
<- disjoint-lookup-contradiction D (lookup/> L1 N1P+1+N3=N2P) L2 F.
%worlds () (disjoint-lookup-contradiction _ _ _ _).
%total (D) (disjoint-lookup-contradiction D _ _ _).
%theorem shift-left-preserves-disjoint :
forall* {N} {D} {M1} {M2} {SM1}
forall {A:disjoint M1 M2} {S1:shift N M1 SM1}
exists {SA:disjoint SM1 (map/+ N D M2)}
true.
- : shift-left-preserves-disjoint _ shift/0 disjoint/L.
- : shift-left-preserves-disjoint M111*M2 (shift/+ N+1+N1=N1P)
(disjoint/> M111*M2 N1+1+N=N1P)
<- plus-swap-succ N+1+N1=N1P N+N1+1=N1P
<- plus-commutative N+N1+1=N1P N1+1+N=N1P.
%worlds () (shift-left-preserves-disjoint _ _ _).
%total { } (shift-left-preserves-disjoint _ _ _).
%theorem shift-left-preserves-disjoint-converse :
forall* {N} {D} {M1} {M2} {SM1}
forall {SA:disjoint SM1 (map/+ N D M2)} {S1:shift N M1 SM1}
exists {A:disjoint M1 M2}
true.
- : shift-left-preserves-disjoint-converse _ shift/0 disjoint/L.
- : shift-left-preserves-disjoint-converse M111*M222 (shift/+ N2+1+N3=N1)
M311*M2
<- plus-swap-succ N2+1+N3=N1 N2+N3+1=N1
<- plus-commutative N2+N3+1=N1 N3+1+N2=N1
<- disjoint/>-inversion M111*M222 N3+1+N2=N1 M311*M2.
%worlds () (shift-left-preserves-disjoint-converse _ _ _).
%total { } (shift-left-preserves-disjoint-converse _ _ _).
%theorem shift-right-preserves-disjoint :
forall* {N} {D} {M1} {M2} {SM2}
forall {A:disjoint M1 M2} {S2:shift N M2 SM2}
exists {SA:disjoint (map/+ N D M1) SM2}
true.
- : shift-right-preserves-disjoint _ shift/0 disjoint/R.
- : shift-right-preserves-disjoint M1*M222 (shift/+ N+1+N2=N2P)
(disjoint/< M1*M222 N2+1+N=N2P)
<- plus-swap-succ N+1+N2=N2P N+N2+1=N2P
<- plus-commutative N+N2+1=N2P N2+1+N=N2P.
%worlds () (shift-right-preserves-disjoint _ _ _).
%total { } (shift-right-preserves-disjoint _ _ _).
%theorem shift-right-preserves-disjoint-converse :
forall* {N} {D} {M1} {M2} {SM2}
forall {SA:disjoint (map/+ N D M1) SM2} {S2:shift N M2 SM2}
exists {A:disjoint M1 M2}
true.
- : shift-right-preserves-disjoint-converse _ shift/0 disjoint/R.
- : shift-right-preserves-disjoint-converse M111*M322 (shift/+ N1+1+N2=N3)
M1*M222
<- plus-swap-succ N1+1+N2=N3 N1+N2+1=N3
<- plus-commutative N1+N2+1=N3 N2+1+N1=N3
<- disjoint/<-inversion M111*M322 N2+1+N1=N3 M1*M222.
%worlds () (shift-right-preserves-disjoint-converse _ _ _).
%total { } (shift-right-preserves-disjoint-converse _ _ _).
%theorem shift-preserves-disjoint :
forall* {N} {M1} {M2} {SM1} {SM2}
forall {A:disjoint M1 M2}
{S1:shift N M1 SM1} {S2:shift N M2 SM2}
exists {SA:disjoint SM1 SM2}
true.
- : shift-preserves-disjoint _ shift/0 _ disjoint/L.
- : shift-preserves-disjoint _ _ shift/0 disjoint/R.
- : shift-preserves-disjoint (disjoint/< M1*M022 N0+1+N1=N2)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/< M1*M022 N0+1+N4=N5)
<- plus-swap-succ N+1+N1=N4 N+N1+1=N4
<- plus-commutative N+N1+1=N4 N1+1+N=N4
<- plus-commutative N0+1+N1=N2 N1+N0+1=N2
<- plus-associative-converse* N1+N0+1=N2 N+1+N2=N5 N+1+N1=N4 N4+N0+1=N5
<- plus-commutative N4+N0+1=N5 N0+1+N4=N5.
- : shift-preserves-disjoint (disjoint/> M311*M2 N3+1+N2=N1)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/> M311*M2 N3+1+N5=N4)
<- plus-swap-succ N+1+N2=N5 N+N2+1=N5
<- plus-commutative N+N2+1=N5 N2+1+N=N5
<- plus-commutative N3+1+N2=N1 N2+N3+1=N1
<- plus-associative-converse* N2+N3+1=N1 N+1+N1=N4 N+1+N2=N5 N5+N3+1=N4
<- plus-commutative N5+N3+1=N4 N3+1+N5=N4.
%worlds () (shift-preserves-disjoint _ _ _ _).
%total { } (shift-preserves-disjoint _ _ _ _).
%theorem shift-preserves-disjoint-converse :
forall* {N} {M1} {M2} {SM1} {SM2}
forall {SA:disjoint SM1 SM2}
{S1:shift N M1 SM1} {S2:shift N M2 SM2}
exists {A:disjoint M1 M2}
true.
- : shift-preserves-disjoint-converse _ shift/0 _ disjoint/L.
- : shift-preserves-disjoint-converse _ _ shift/0 disjoint/R.
- : shift-preserves-disjoint-converse (disjoint/< M1*M055 N0+1+N4=N5)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/< M1*M055 N0+1+N1=N2)
<- plus-commutative N+1+N1=N4 N1+N+1=N4
<- plus-swap-succ-converse N1+N+1=N4 N1+1+N=N4
<- plus-associative-converse N1+N+1=N4 N0+1+N4=N5 N2P N0+1+N1=N2P N2P+N+1=N5
<- plus-commutative N+1+N2=N5 N2+N+1=N5
<- plus-right-cancels N2P+N+1=N5 N2+N+1=N5 nat`eq/ nat`eq/ N2P=N2
<- plus-respects-eq N0+1+N1=N2P nat`eq/ nat`eq/ N2P=N2 N0+1+N1=N2.
- : shift-preserves-disjoint-converse (disjoint/> M611*M2 N6+1+N5=N4)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/> M611*M2 N6+1+N2=N1)
<- plus-commutative N+1+N2=N5 N2+N+1=N5
<- plus-swap-succ-converse N2+N+1=N5 N2+1+N=N5
<- plus-associative-converse N2+N+1=N5 N6+1+N5=N4 N1P N6+1+N2=N1P N1P+N+1=N4
<- plus-commutative N+1+N1=N4 N1+N+1=N4
<- plus-right-cancels N1P+N+1=N4 N1+N+1=N4 nat`eq/ nat`eq/ N1P=N1
<- plus-respects-eq N6+1+N2=N1P nat`eq/ nat`eq/ N1P=N1 N6+1+N2=N1.
%worlds () (shift-preserves-disjoint-converse _ _ _ _).
%total { } (shift-preserves-disjoint-converse _ _ _ _).
%theorem ne-implies-disjoint :
forall* {N1} {D1} {N2} {D2}
forall {NE:nat`ne N1 N2}
exists {D:disjoint (map/+ N1 D1 map/0) (map/+ N2 D2 map/0)}
true.
- : ne-implies-disjoint (nat`ne/< N1 N1>N2)
(disjoint/> disjoint/R N3+1+N2=N1)
<- gt-implies-plus N1>N2 _ N3+1+N2=N1.
%worlds () (ne-implies-disjoint _ _).
%total { } (ne-implies-disjoint _ _).
%%% Theorems about size
%theorem false-implies-size :
forall* {M} {N}
forall {F:void}
exists {SZ:size M N}
true.
%worlds () (false-implies-size _ _).
%total { } (false-implies-size _ _).
%theorem size-total* :
forall {M}
exists {N} {MX:size M N}
true.
- : size-total* map/0 _ size/0.
- : size-total* _ _ (size/+ SZ)
<- size-total* _ _ SZ.
%worlds () (size-total* _ _ _).
%total (M) (size-total* M _ _).
%abbrev size-total = size-total* _ _.
%theorem size-deterministic :
forall* {M1} {M2} {N1} {N2}
forall {SZ1:size M1 N1} {SZ2:size M2 N2} {EM:eq M1 M2}
exists {EN:nat`eq N1 N2}
true.
- : size-deterministic size/0 size/0 eq/ nat`eq/.
- : size-deterministic (size/+ N1=|M1|) (size/+ N2=|M2|) eq/ N1+1=N2+1
<- size-deterministic N1=|M1| N2=|M2| eq/ N1=N2
<- succ-deterministic N1=N2 N1+1=N2+1.
%worlds () (size-deterministic _ _ _ _).
%total (S) (size-deterministic S _ _ _).
%%% Theorems about bound
%theorem false-implies-bound :
forall* {M} {N}
forall {F:void}
exists {MX:bound M N}
true.
%worlds () (false-implies-bound _ _).
%total { } (false-implies-bound _ _).
%theorem bound-total* :
forall {M}
exists {N} {MX:bound M N}
true.
- : bound-total* map/0 _ bound/0.
- : bound-total* _ _ (bound/+ P MX)
<- bound-total* _ _ MX
<- plus-total P.
%worlds () (bound-total* _ _ _).
%total (M) (bound-total* M _ _).
%abbrev bound-total = bound-total* _ _.
%theorem ge-bound-implies-not-member :
forall* {M} {X} {N}
forall {B:bound M X} {G:nat`ge N X}
exists {F:not-member M N}
true.
- : ge-bound-implies-not-member bound/0 _ not-member/0.
- : ge-bound-implies-not-member (bound/+ M1+1+X1=X B) N>=X (not-member/> F1 N1+1+M1=N)
<- nat`ge-implies-plus N>=X Y1 Y1+X=N
<- nat`plus-commutative M1+1+X1=X X1+M1+1=X
<- nat`plus-associative-converse X1+M1+1=X Y1+X=N N1 Y1+X1=N1 N1+M1+1=N
<- plus-swap-succ-converse N1+M1+1=N N1+1+M1=N
<- plus-implies-ge Y1+X1=N1 N1>=X1
<- ge-bound-implies-not-member B N1>=X1 F1.
%worlds () (ge-bound-implies-not-member _ _ _).
%total (B) (ge-bound-implies-not-member B _ _).
%%% Theorems about shift
%theorem false-implies-shift :
forall* {M} {N} {M'}
forall {F:void}
exists {S:shift N M M'}
true.
%worlds () (false-implies-shift _ _).
%total { } (false-implies-shift _ _).
%theorem shift-respects-eq :
forall* {N} {M1} {M2} {N'} {M1'} {M2'}
forall {S:shift N M1 M2}
{EN:nat`eq N N'} {E1:eq M1 M1'} {E2:eq M2 M2'}
exists {S':shift N' M1' M2'}
true.
- : shift-respects-eq S nat`eq/ eq/ eq/ S.
%worlds () (shift-respects-eq _ _ _ _ _).
%total { } (shift-respects-eq _ _ _ _ _).
%theorem shift-total* :
forall {N} {M1}
exists {M2} {S:shift N M1 M2}
true.
- : shift-total* N map/0 map/0 shift/0.
- : shift-total* N1 (map/+ N2 D M) (map/+ N3 D M) (shift/+ N1+1+N2=N3)
<- plus-total N1+1+N2=N3.
%worlds () (shift-total* _ _ _ _).
%total { } (shift-total* _ _ _ _).
%abbrev shift-total = shift-total* _ _ _.
%theorem shift-deterministic :
forall* {N} {M1} {M2} {N'} {M1'} {M2'}
forall {S:shift N M1 M2} {S':shift N' M1' M2'}
{EN:nat`eq N N'} {EM1:eq M1 M1'}
exists {EM2:eq M2 M2'}
true.
- : shift-deterministic shift/0 shift/0 nat`eq/ eq/ eq/.
- : shift-deterministic (shift/+ N1+1+N2=N3) (shift/+ N1+1+N2=N3') nat`eq/ eq/ E
<- plus-deterministic N1+1+N2=N3 N1+1+N2=N3' nat`eq/ nat`eq/ N3=N3P
<- map/+-preserves-eq N3=N3P unit`eq/ eq/ E.
%worlds () (shift-deterministic _ _ _ _ _).
%total { } (shift-deterministic _ _ _ _ _).
%theorem shifts-add :
forall* {N1} {N2} {N3} {M0} {M1} {M3}
forall {S1:shift N1 M0 M1} {S2:shift N2 M1 M3} {P:plus (s N1) N2 N3}
exists {S3:shift N3 M0 M3}
true.
- : shifts-add shift/0 shift/0 _ shift/0.
- : shifts-add (shift/+ N1+1+N4=N5) (shift/+ N2+1+N5=N7) N1+1+N2=N3
(shift/+ N3+1+N4=N7)
<- plus-total N3+1+N4=N7'
<- plus-swap-succ N3+1+N4=N7' N3+N4+1=N7'
<- plus-swap-succ N1+1+N2=N3 N1+N2+1=N3
<- plus-swap-succ N1+1+N4=N5 N1+N4+1=N5
<- plus-commutative N1+N2+1=N3 N2+1+N1=N3
<- plus-associative* N2+1+N1=N3 N3+N4+1=N7' N1+N4+1=N5 N2+1+N5=N7'
<- plus-deterministic N2+1+N5=N7' N2+1+N5=N7 nat`eq/ nat`eq/ N7'=N7
<- plus-respects-eq N3+1+N4=N7' nat`eq/ nat`eq/ N7'=N7 N3+1+N4=N7.
%worlds () (shifts-add _ _ _ _).
%total { } (shifts-add _ _ _ _).
%theorem shifts-add-converse :
forall* {N1} {N2} {N3} {M0} {M3}
forall {S3:shift N3 M0 M3} {P:plus (s N1) N2 N3}
exists {M1} {S1:shift N1 M0 M1} {S2:shift N2 M1 M3}
true.
- : shifts-add-converse S3 P M1 S1 S2
<- shift-total S1
<- shift-total S2'
<- shifts-add S1 S2' P S3'
<- shift-deterministic S3' S3 nat`eq/ eq/ M3'=M3
<- shift-respects-eq S2' nat`eq/ eq/ M3'=M3 S2.
%worlds () (shifts-add-converse _ _ _ _ _).
%total { } (shifts-add-converse _ _ _ _ _).
%theorem shift-preserves-lookup :
forall* {M1} {N1} {D} {N0} {M2}
forall {L1:lookup M1 N1 D} {S:shift N0 M1 M2}
exists {N2} {P:plus (s N0) N1 N2} {L2:lookup M2 N2 D}
true.
- : shift-preserves-lookup (lookup/= nat`eq/) (shift/+ N0+1+N1=N2) _
N0+1+N1=N2 (lookup/= nat`eq/).
- : shift-preserves-lookup (lookup/> L N3+1+N1=N4) (shift/+ N0+1+N1=N2) _
N0+1+N4=N5 (lookup/> L N3+1+N2=N5)
<- plus-total N0+1+N4=N5
<- plus-commutative N3+1+N1=N4 N1+N3+1=N4
<- plus-associative-converse* N1+N3+1=N4 N0+1+N4=N5 N0+1+N1=N2 N2+N3+1=N5
<- plus-commutative N2+N3+1=N5 N3+1+N2=N5.
%worlds () (shift-preserves-lookup _ _ _ _ _).
%total { } (shift-preserves-lookup _ _ _ _ _).
%theorem shift-preserves-lookup* :
forall* {M1} {N1} {D} {N0} {M2} {N2}
forall {L1:lookup M1 N1 D} {S:shift N0 M1 M2}
{P:plus (s N0) N1 N2}
exists {L2:lookup M2 N2 D}
true.
- : shift-preserves-lookup* L1 S P L2
<- shift-preserves-lookup L1 S _ P' L2'
<- plus-deterministic P' P nat`eq/ nat`eq/ N2'=N2
<- lookup-respects-eq L2' eq/ N2'=N2 unit`eq/ L2.
%worlds () (shift-preserves-lookup* _ _ _ _).
%total { } (shift-preserves-lookup* _ _ _ _).
%theorem shift-preserves-lookup-converse :
forall* {M1} {N0} {D} {N2} {M2}
forall {L2:lookup M2 N2 D} {S:shift N0 M1 M2}
exists {N1} {P:plus (s N0) N1 N2} {L1:lookup M1 N1 D}
true.
- : shift-preserves-lookup-converse (lookup/= nat`eq/) (shift/+ N0+1+N1=N2) _
N0+1+N1=N2 (lookup/= nat`eq/).
- : shift-preserves-lookup-converse (lookup/> L N3+1+N2=N5) (shift/+ N0+1+N1=N2)
_ N0+1+N4=N5 (lookup/> L N3+1+N1=N4)
<- plus-commutative N0+1+N1=N2 N1+N0+1=N2
<- plus-associative-converse N1+N0+1=N2 N3+1+N2=N5 N4 N3+1+N1=N4 N4+N0+1=N5
<- plus-commutative N4+N0+1=N5 N0+1+N4=N5.
%worlds () (shift-preserves-lookup-converse _ _ _ _ _).
%total { } (shift-preserves-lookup-converse _ _ _ _ _).
%theorem shift-preserves-lookup-converse* :
forall* {M1} {N1} {D} {N2} {M2} {N0}
forall {L2:lookup M2 N2 D} {S:shift N0 M1 M2}
{P:plus (s N0) N1 N2}
exists {L1:lookup M1 N1 D}
true.
- : shift-preserves-lookup-converse* L2 S P L1
<- shift-preserves-lookup-converse L2 S _ P' L1'
<- plus-left-cancels P' P nat`eq/ nat`eq/ N1'=N1
<- lookup-respects-eq L1' eq/ N1'=N1 unit`eq/ L1.
%worlds () (shift-preserves-lookup-converse* _ _ _ _).
%total { } (shift-preserves-lookup-converse* _ _ _ _).
%theorem shift-preserves-update :
forall* {M1} {N1} {D} {M1'} {N0} {M2}
forall {U1:update M1 N1 D M1'}
{S:shift N0 M1 M2}
exists {N2} {M2'}
{P:plus (s N0) N1 N2}
{SS:shift N0 M1' M2'}
{U2:update M2 N2 D M2'}
true.
- : shift-preserves-update update/0 shift/0 _ _ P (shift/+ P) update/0
<- plus-total P.
- : shift-preserves-update (update/= nat`eq/) (shift/+ P) _ _ P (shift/+ P)
(update/= nat`eq/).
- : shift-preserves-update (update/< N4+1+N1=N3) (shift/+ N0+1+N3=N5) _ _
N0+1+N1=N2 (shift/+ N0+1+N1=N2)
(update/< N4+1+N2=N5)
<- plus-commutative N4+1+N1=N3 N1+N4+1=N3
<- plus-associative-converse N1+N4+1=N3 N0+1+N3=N5 _ N0+1+N1=N2 N2+N4+1=N5
<- plus-commutative N2+N4+1=N5 N4+1+N2=N5.
- : shift-preserves-update (update/> U N4+1+N3=N1) (shift/+ N0+1+N3=N5) _ _
N0+1+N1=N2 (shift/+ N0+1+N3=N5)
(update/> U N4+1+N5=N2)
<- plus-total N0+1+N1=N2
<- plus-commutative N4+1+N3=N1 N3+N4+1=N1
<- plus-associative-converse* N3+N4+1=N1 N0+1+N1=N2 N0+1+N3=N5 N5+N4+1=N2
<- plus-commutative N5+N4+1=N2 N4+1+N5=N2.
%worlds () (shift-preserves-update _ _ _ _ _ _ _).
%total { } (shift-preserves-update _ _ _ _ _ _ _).
%theorem shift-preserves-size :
forall* {M} {N1} {N2} {S2M}
forall {SZ:size M N1} {SH:shift N2 M S2M}
exists {SHSZ:size S2M N1}
true.
- : shift-preserves-size size/0 shift/0 size/0.
- : shift-preserves-size (size/+ SZ) (shift/+ _) (size/+ SZ).
%worlds () (shift-preserves-size _ _ _).
%total { } (shift-preserves-size _ _ _).
%%% Theorems about disjoint?
%theorem disjoint?-total* :
forall {M1} {M2}
exists {B} {D:disjoint? M1 M2 B}
true.
- : disjoint?-total* _ _ _ (disjoint?/yes disjoint/L).
- : disjoint?-total* _ _ _ (disjoint?/yes disjoint/R).
%theorem disjoint?-total*/+ :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {C}
forall {S1} {S2} {SZ1:size M1 S1} {SZ2:size M2 S2} {CMP:nat`compare N1 N2 C}
exists {B} {D:disjoint? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
%theorem disjoint?-total*/< :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0} {B1}
forall {P:plus (s N0) N1 N2}
{D?1:disjoint? M1 (map/+ N0 D2 M2) B1}
exists {B} {D:disjoint? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
%theorem disjoint?-total*/> :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3} {B1}
forall {P:plus (s N3) N2 N1}
{D?1:disjoint? (map/+ N3 D1 M1) M2 B1}
exists {B} {D:disjoint? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
- : disjoint?-total* _ _ _ D?
<- size-total SZ1
<- size-total SZ2
<- nat`compare-total CMP
<- disjoint?-total*/+ _ _ SZ1 SZ2 CMP _ D?.
- : disjoint?-total*/+ _ _ _ _ (nat`compare/=) _
(disjoint?/no (lookup/= nat`eq/) (lookup/= nat`eq/)).
- : disjoint?-total*/+ _ _ _ _ (nat`compare/< N2>N1) _ D?
<- gt-implies-plus N2>N1 _ N0+1+N1=N2
<- disjoint?-total*/< N0+1+N1=N2 (disjoint?/yes disjoint/L) _ D?.
- : disjoint?-total*/+ _ _ (size/+ SZ1) SZ2 (nat`compare/< N2>N1) _ D?
<- gt-implies-plus N2>N1 _ N0+1+N1=N2
<- nat`compare-total CMP
<- disjoint?-total*/+ _ _ SZ1 SZ2 CMP _ D?1
<- disjoint?-total*/< N0+1+N1=N2 D?1 _ D?.
- : disjoint?-total*/< N0+1+N1=N2 (disjoint?/yes M1*M022) _
(disjoint?/yes (disjoint/< M1*M022 N0+1+N1=N2)).
- : disjoint?-total*/< N0+1+N1=N2 (disjoint?/no M1^N3=D1 M022^N3=D2) _
(disjoint?/no (lookup/> M1^N3=D1 N3+1+N1=N4) M222^N4=D2)
<- plus-total N3+1+N1=N4
<- plus-swap-succ N3+1+N1=N4 N3+N1+1=N4
<- plus-commutative N3+N1+1=N4 N1+1+N3=N4
<- plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- plus-commutative N0+N1+1=N2 N1+1+N0=N2
<- shift-preserves-lookup* M022^N3=D2 (shift/+ N1+1+N0=N2) N1+1+N3=N4
M222^N4=D2.
%worlds () (disjoint?-total*/< _ _ _ _).
%total { } (disjoint?-total*/< _ _ _ _).
- : disjoint?-total*/+ _ _ _ _ (nat`compare/> N1>N2) _ D?
<- gt-implies-plus N1>N2 _ N3+1+N2=N1
<- disjoint?-total*/> N3+1+N2=N1 (disjoint?/yes disjoint/R) _ D?.
- : disjoint?-total*/+ _ _ SZ1 (size/+ SZ2) (nat`compare/> N1>N2) _ D?
<- gt-implies-plus N1>N2 _ N3+1+N2=N1
<- nat`compare-total CMP
<- disjoint?-total*/+ _ _ SZ1 SZ2 CMP _ D?1
<- disjoint?-total*/> N3+1+N2=N1 D?1 _ D?.
- : disjoint?-total*/> P (disjoint?/yes D) _ (disjoint?/yes (disjoint/> D P)).
- : disjoint?-total*/> N3+1+N2=N1 (disjoint?/no M311^N4=D1 M2^N4=D2) _
(disjoint?/no M111^N5=D1 (lookup/> M2^N4=D2 N4+1+N2=N5))
<- plus-total N4+1+N2=N5
<- plus-swap-succ N4+1+N2=N5 N4+N2+1=N5
<- plus-commutative N4+N2+1=N5 N2+1+N4=N5
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-commutative N3+N2+1=N1 N2+1+N3=N1
<- shift-preserves-lookup* M311^N4=D1 (shift/+ N2+1+N3=N1) N2+1+N4=N5
M111^N5=D1.
%worlds () (disjoint?-total*/> _ _ _ _).
%total { } (disjoint?-total*/> _ _ _ _).
%worlds () (disjoint?-total*/+ _ _ _ _ _ _ _).
%total [S1 S2] (disjoint?-total*/+ S1 S2 _ _ _ _ _).
%worlds () (disjoint?-total* _ _ _ _).
%total { } (disjoint?-total* _ _ _ _).
%abbrev disjoint?-total = disjoint?-total* _ _ _.
%%% Theorems about update
%theorem false-implies-update :
forall* {M} {N} {D} {M'}
forall {F:void}
exists {U:update M N D M'}
true.
%worlds () (false-implies-update _ %{=>}% M^N=D->M').
%total {} (false-implies-update _ _).
%theorem update-respects-eq :
forall* {M1} {N} {D} {M2} {M1P} {NP} {DP} {M2P}
forall {U:update M1 N D M2} {EM1:eq M1 M1P}
{EN:nat`eq N NP} {ED:unit`eq D DP} {EM2:eq M2 M2P}
exists {UP:update M1P NP DP M2P}
true.
- : update-respects-eq U eq/ nat`eq/ unit`eq/ eq/ U.
%worlds () (update-respects-eq M1^N=D->M2 M1=M1' N=N' D=D' M2=M2'
%{=>}% M1'^N'=D'->M2').
%total {} (update-respects-eq _ _ _ _ _ _).
%reduces U = U' (update-respects-eq U _ _ _ _ U').
%%% technical lemmas to help prove reduction arguments
update-eq : {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'}
update M1 N1 D1 M1' -> update M2 N2 D2 M2' -> type.
update-eq/ : update-eq M1 N1 D1 M1' M1 N1 D1 M1' U U.
%theorem false-implies-update-eq :
forall* {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'} {U} {U'}
forall {F:void}
exists {UE:update-eq M1 N1 D1 M1' M2 N2 D2 M2' U U'}
true.
%worlds () (false-implies-update-eq _ _).
%total { } (false-implies-update-eq _ _).
%theorem meta-update-eq :
forall* {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'}
forall {U} {U'} {UE:update-eq M1 N1 D1 M1' M2 N2 D2 M2' U U'}
true.
- : meta-update-eq U U (update-eq/).
%worlds () (meta-update-eq _ _ _).
%total { } (meta-update-eq _ _ _).
%reduces U = U' (meta-update-eq U U' _).
%%% inversion lemmas
%theorem update/=-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2}
forall {U:update (map/+ N1 D1 M1) N2 D2 M2} {E:nat`eq N1 N2}
exists {EM:eq (map/+ N2 D2 M1) M2}
true.
- : update/=-inversion (update/= nat`eq/) nat`eq/ eq/.
- : update/=-inversion (update/< N3+1+N=N) nat`eq/ E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update/=-inversion (update/> U1022 N3+1+N=N) nat`eq/ E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
%worlds () (update/=-inversion _ _ _).
%total { } (update/=-inversion _ _ _).
%theorem update/<-inversion:
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3}
forall {U:update (map/+ N1 D1 M1) N2 D2 M2} {P:plus (s N3) N2 N1}
exists {E:eq (map/+ N2 D2 (map/+ N3 D1 M1)) M2}
true.
- : update/<-inversion (update/= nat`eq/) N3+1+N=N E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update/<-inversion (update/< N3+1+N2=N1) N3P+1+N2=N1 E
<- nat`plus-right-cancels N3P+1+N2=N1 N3+1+N2=N1 nat`eq/ nat`eq/ N3P+1=N3+1
<- nat`succ-cancels N3P+1=N3+1 N3P=N3
<- map/+-preserves-eq N3P=N3 unit`eq/ eq/ M311P=M311
<- map/+-preserves-eq nat`eq/ unit`eq/ M311P=M311 E.
- : update/<-inversion (update/> _ N0+1+N1=N2) N3+1+N2=N1 E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (update/<-inversion _ _ _).
%total { } (update/<-inversion _ _ _).
%theorem update/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M} {N0}
forall {U:update (map/+ N1 D1 M1) N2 D2 M} {P:plus (s N0) N1 N2}
exists {M2} {UP:update M1 N0 D2 M2} {E:eq (map/+ N1 D1 M2) M}
true.
% a little more complex than might be expected
% because we want to prove reduction
- : update/>-inversion (update/= nat`eq/: update (map/+ N D1 M1) N D2
(map/+ N D2 M1))
N0+1+N=N M1 U' E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E
<- false-implies-update F U'
<- false-implies-update-eq F
(UE:update-eq (map/+ N D1 M1) N D2 (map/+ N D2 M1)
(map/+ N D1 M1) N D2 (map/+ N D1 M1) _ _)
<- meta-update-eq (update/= nat`eq/) (update/> U' N0+1+N=N) UE.
- : update/>-inversion (update/< N3+1+N2=N1: update (map/+ N1 D1 M1) _ _ _)
N0+1+N1=N2 M1 U' E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-update F U'
<- false-implies-eq F E
<- false-implies-update-eq F
(UE:update-eq (map/+ N1 D1 M1) N2 D2 (map/+ N2 D2 (map/+ N3 D1 M1))
(map/+ N1 D1 M1) N2 D2 (map/+ N1 D1 M1) _ _)
<- meta-update-eq (update/< N3+1+N2=N1) (update/> U' N0+1+N1=N2) UE.
- : update/>-inversion (update/> U N0+1+N1=N2) N0P+1+N1=N2 _ UP eq/
<- nat`plus-right-cancels N0+1+N1=N2 N0P+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0P+1
<- nat`succ-cancels N0+1=N0P+1 N0=N0P
<- update-respects-eq U eq/ N0=N0P unit`eq/ eq/ UP.
%worlds () (update/>-inversion _ _ _ _ _).
%total { } (update/>-inversion _ _ _ _ _).
%reduces U' < U (update/>-inversion U _ _ U' _).
%theorem update-deterministic :
forall* {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'}
forall {U1:update M1 N1 D1 M1'} {U2:update M2 N2 D2 M2'}
{EM:eq M1 M2} {EN:nat`eq N1 N2} {ED:unit`eq D1 D2}
exists {EM':eq M1' M2'}
true.
- : update-deterministic update/0 update/0 eq/ nat`eq/ unit`eq/ eq/.
- : update-deterministic (update/= nat`eq/) (update/= nat`eq/) eq/ nat`eq/ unit`eq/ eq/.
- : update-deterministic (update/< N3+1+N2=N1) (update/< N3'+1+N2=N1)
eq/ nat`eq/ unit`eq/ M1'=M2'
<- plus-right-cancels N3+1+N2=N1 N3'+1+N2=N1 nat`eq/ nat`eq/ SN3=SN3'
<- succ-cancels SN3=SN3' N3E
<- map/+-preserves-eq N3E unit`eq/ eq/ MM1=MM2
<- map/+-preserves-eq nat`eq/ unit`eq/ MM1=MM2 M1'=M2'.
- : update-deterministic (update/> F1^N0=D2->F2 N0+1+N1=N2)
(update/> F1^N0'=D2->F2' N0'+1+N1=N2)
eq/ nat`eq/ unit`eq/ M1'=M2'
<- plus-right-cancels N0+1+N1=N2 N0'+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0'
<- update-deterministic F1^N0=D2->F2 F1^N0'=D2->F2' eq/ N0=N0'
unit`eq/ F2=F2'
<- map/+-preserves-eq nat`eq/ unit`eq/ F2=F2' M1'=M2'.
%% contradiction cases:
- : update-deterministic (update/= nat`eq/) (update/< N3+1+N=N) eq/ nat`eq/ unit`eq/ E
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/= nat`eq/) (update/> _ N0+1+N=N) eq/ nat`eq/ unit`eq/ E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/< N3+1+N=N) (update/= nat`eq/) eq/ nat`eq/ unit`eq/ E
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/< N3+1+N2=N1) (update/> _ N0+1+N1=N2)
eq/ nat`eq/ unit`eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
- : update-deterministic (update/> _ N0+1+N=N) (update/= nat`eq/) eq/ nat`eq/ unit`eq/ E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/> _ N0+1+N1=N2) (update/< N3+1+N2=N1)
eq/ nat`eq/ unit`eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (update-deterministic M1^N1=D1->M1' M2^N2=D2->M2' M1=M2 N1=N2 D1=D2
%{=>}% M1'=M2').
%total (U) (update-deterministic U _ _ _ _ _).
%theorem update-total* :
forall {M} {N} {D}
exists {M'} {U:update M N D M'}
true.
%% we need a mutually recursive lemma
%theorem update-map/+-total :
forall {N1} {D1} {M1} {N2} {D2} {C} {CMP:nat`compare N1 N2 C}
exists {M2} {U:update (map/+ N1 D1 M1) N2 D2 M2}
true.
- : update-total* map/0 N D (map/+ N D map/0) update/0.
- : update-total* (map/+ N1 D1 M1) N2 D2 M2 U
<- nat`compare-total* N1 N2 C CMP
<- update-map/+-total N1 D1 M1 N2 D2 C CMP M2 U.
- : update-map/+-total N1 D1 M1 N2 D2 equal CMP (map/+ N2 D2 M1) (update/= N1=N2)
<- equal-implies-eq CMP N1=N2.
- : update-map/+-total N1 D1 M1 N2 D2 less CMP (map/+ N1 D1 M1')
(update/> U1 N0+1+N1=N2)
<- less-implies-lt CMP N2>N1
<- gt-implies-plus N2>N1 N0 N0+1+N1=N2
<- update-total* M1 N0 D2 M1' U1.
- : update-map/+-total N1 D1 M1 N2 D2 greater CMP (map/+ N2 D2 (map/+ N3 D1 M1))
(update/< N3+1+N2=N1)
<- greater-implies-gt CMP N1>N2
<- gt-implies-plus N1>N2 N3 N3+1+N2=N1.
%worlds () (update-total* M N D %{=>}% M' M^N=D->M')
(update-map/+-total _ _ _ _ _ _ _ _ _).
%total (M1 M2) (update-total* M1 _ _ _ _) (update-map/+-total _ _ M2 _ _ _ _ _ _).
%abbrev update-total = update-total* _ _ _ _.
%theorem lookup-implies-update :
forall* {F} {N} {D}
forall {L:lookup F N D}
exists {U:update F N D F}
true.
- : lookup-implies-update (lookup/= nat`eq/) (update/= nat`eq/).
- : lookup-implies-update (lookup/> L P) (update/> U P)
<- lookup-implies-update L U.
%worlds () (lookup-implies-update _ _).
%total (L) (lookup-implies-update L _).
%theorem update-implies-lookup :
forall* {F} {N} {D} {F'}
forall {U:update F N D F'}
exists {L:lookup F' N D}
true.
- : update-implies-lookup update/0 (lookup/= nat`eq/).
- : update-implies-lookup (update/= nat`eq/) (lookup/= nat`eq/).
- : update-implies-lookup (update/< _) (lookup/= nat`eq/).
- : update-implies-lookup (update/> F^N0=D2->F' N0+1+N1=N2)
(lookup/> F'^N0=D2 N0+1+N1=N2)
<- update-implies-lookup F^N0=D2->F' F'^N0=D2.
%worlds () (update-implies-lookup F^N=D->F' %{=>}% F'^N=D).
%total (U) (update-implies-lookup U _).
%theorem update-preserves-lookup :
forall* {F} {N1} {D1} {F'} {N2} {D2}
forall {L:lookup F N2 D2} {U:update F N1 D1 F'} {X:nat`ne N2 N1}
exists {L':lookup F' N2 D2}
true.
%% update/0 is impossible
- : update-preserves-lookup (lookup/= nat`eq/) (update/= nat`eq/) N<>N L'
<- nat`ne-anti-reflexive N<>N FALSE
<- false-implies-lookup FALSE L'.
- : update-preserves-lookup (lookup/> L1 P1) (update/= nat`eq/) _ (lookup/> L1 P1).
- : update-preserves-lookup (lookup/= nat`eq/) (update/< N3+1+N2=N1) _
(lookup/> (lookup/= nat`eq/) N3+1+N2=N1).
- : update-preserves-lookup (lookup/> L N0+1+N1=N2') (update/< N3+1+N2=N1) _
(lookup/> (lookup/> L N0+1+N3=N4)
N4+1+N2=N2')
<- plus-left-decrease N3+1+N2=N1 N1-1 N1=N1-1+1 N3+N2=N1-1
<- plus-right-increase N3+N2=N1-1 N3+N2+1=N1-1+1
<- nat`eq-symmetric N1=N1-1+1 N1-1+1=N1
<- plus-respects-eq N3+N2+1=N1-1+1 nat`eq/ nat`eq/ N1-1+1=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 N0+1+N1=N2' N4 N0+1+N3=N4
N4+N2+1=N2'
<- plus-swap-succ-converse N4+N2+1=N2' N4+1+N2=N2'.
- : update-preserves-lookup (lookup/= nat`eq/) (update/> _ _) _ (lookup/= nat`eq/).
- : update-preserves-lookup (lookup/> L N0+1+N1=N2)
((update/> U N0'+1+N1=N2')
: update (map/+ N1 D1 M1) N2' D'
(map/+ N1 D1 M1'))
N2<>N2'
((lookup/> L' N0+1+N1=N2)
: lookup (map/+ N1 D1 M1') N2 D)
<- plus-right-cancels-ne N0+1+N1=N2 N0'+1+N1=N2' nat`eq/ N2<>N2' N0+1<>N0'+1
<- succ-preserves-ne-converse N0+1<>N0'+1 N0<>N0'
<- update-preserves-lookup L U N0<>N0' L'.
%worlds () (update-preserves-lookup F^N2=D2 F^N1=D1->F' N1<>N2 F'^N2=D2).
%total (L) (update-preserves-lookup L _ _ _).
%theorem update-preserves-lookup-converse :
forall* {F1} {N1} {D1} {F2} {N2} {D2}
forall {L2:lookup F2 N2 D2} {U:update F1 N1 D1 F2} {X:nat`ne N2 N1}
exists {L1:lookup F1 N2 D2}
true.
- : update-preserves-lookup-converse (lookup/= nat`eq/) update/0 N<>N L1
<- nat`ne-anti-reflexive N<>N F
<- false-implies-lookup F L1.
- : update-preserves-lookup-converse (lookup/= nat`eq/) (update/= nat`eq/) N<>N
L1
<- nat`ne-anti-reflexive N<>N F
<- false-implies-lookup F L1.
- : update-preserves-lookup-converse (lookup/= nat`eq/) (update/< N3+1+N2=N1)
N<>N L1
<- nat`ne-anti-reflexive N<>N F
<- false-implies-lookup F L1.
- : update-preserves-lookup-converse (lookup/= nat`eq/) (update/> _ _) _
(lookup/= nat`eq/).
- : update-preserves-lookup-converse (lookup/> L1 P) (update/= nat`eq/) _
(lookup/> L1 P).
- : update-preserves-lookup-converse (lookup/> (lookup/= nat`eq/) N3+1+N2=N4)
(update/< N3+1+N2=N1) _
(lookup/= N1=N4)
<- plus-deterministic N3+1+N2=N1 N3+1+N2=N4 nat`eq/ nat`eq/ N1=N4.
- : update-preserves-lookup-converse (lookup/> (lookup/> L1 N6+1+N3=N5)
N5+1+N2=N4)
(update/< N3+1+N2=N1) _
(lookup/> L1 N6+1+N1=N4)
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-swap-succ N5+1+N2=N4 N5+N2+1=N4
<- plus-associative* N6+1+N3=N5 N5+N2+1=N4 N3+N2+1=N1 N6+1+N1=N4.
- : update-preserves-lookup-converse (lookup/> L2 N5+1+N1=N4)
(update/> U1 N0+1+N1=N2) N4<>N2
(lookup/> L1 N5+1+N1=N4)
<- plus-right-cancels-ne N5+1+N1=N4 N0+1+N1=N2 nat`eq/ N4<>N2 N5+1<>N0+1
<- succ-preserves-ne-converse N5+1<>N0+1 N5<>N0
<- update-preserves-lookup-converse L2 U1 N5<>N0 L1.
%worlds () (update-preserves-lookup-converse _ _ _ _).
%total (L) (update-preserves-lookup-converse L _ _ _).
%theorem update-preserves-not-member :
forall* {M1} {N1} {N2} {D} {M2}
forall {F1:not-member M1 N1} {U:update M1 N2 D M2} {N:nat`ne N1 N2}
exists {F2:not-member M2 N1}
true.
- : update-preserves-not-member not-member/0 update/0 (nat`ne/< N>M) (not-member/< N>M).
- : update-preserves-not-member not-member/0 update/0 (nat`ne/> M>N)
(not-member/> not-member/0 M1+1+N=M)
<- gt-implies-plus M>N M1 M1+1+N=M.
- : update-preserves-not-member (not-member/< N>M) (update/= nat`eq/) _ (not-member/< N>M).
- : update-preserves-not-member (not-member/< N1>M) (update/< N3+1+N2=N1) (nat`ne/< N2>M)
(not-member/< N2>M).
- : update-preserves-not-member (not-member/< N1>M) (update/< N3+1+N2=N1) (nat`ne/> M>N2)
(not-member/> (not-member/< N3>M1) M1+1+N2=M)
<- gt-implies-plus M>N2 M1 M1+1+N2=M
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-swap-succ M1+1+N2=M M1+N2+1=M
<- plus-right-cancels-gt N3+N2+1=N1 M1+N2+1=M nat`eq/ N1>M N3>M1.
- : update-preserves-not-member (not-member/< N1>M) (update/> _ _) _ (not-member/< N1>M).
- : update-preserves-not-member (not-member/> F P) (update/= nat`eq/) _ (not-member/> F P).
- : update-preserves-not-member (not-member/> F M1+1+N1=M) (update/< N3+1+N2=N1) _
(not-member/> (not-member/> F M1+1+N3=MM) MM+1+N2=M)
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 M1+1+N1=M MM M1+1+N3=MM
MM+N2+1=M
<- plus-swap-succ-converse MM+N2+1=M MM+1+N2=M.
- : update-preserves-not-member (not-member/> F M1+1+N1=M) (update/> U N0+1+N1=N2) M<>N2
(not-member/> F' M1+1+N1=M)
<- plus-right-cancels-ne M1+1+N1=M N0+1+N1=N2 nat`eq/ M<>N2 M1+1<>N0+1
<- succ-preserves-ne-converse M1+1<>N0+1 M1<>N0
<- update-preserves-not-member F U M1<>N0 F'.
%worlds () (update-preserves-not-member N1-not-member-M1 M1^N2=D->M2 N1<>N2 N1-not-member-M2).
%total (F) (update-preserves-not-member F _ _ _).
%theorem update-preserves-not-member-converse :
forall* {M1} {N1} {N2} {D} {M2}
forall {F1:not-member M2 N1} {U:update M1 N2 D M2}
exists {F2:not-member M1 N1}
true.
%theorem update-preserves-not-member-converse-helper :
forall* {M1} {N1} {N2} {D} {M2} {B} {B2}
forall {F1:not-member M2 N1} {U:update M1 N2 D M2}
{D:member? M1 N1 B} {E:nat`eq? N1 N2 B2}
exists {F2:not-member M1 N1}
true.
- : update-preserves-not-member-converse-helper _ _ (member?/out F) _ F.
- : update-preserves-not-member-converse-helper F2 U (member?/in L1) (nat`eq?/no N) F1
<- update-preserves-lookup L1 U N L2
<- not-member-lookup-not-equal F2 L2 N<>N
<- nat`ne-anti-reflexive N<>N F
<- false-implies-not-member F F1.
- : update-preserves-not-member-converse-helper F2 U _ nat`eq?/yes F1
<- update-implies-lookup U L2
<- not-member-lookup-not-equal F2 L2 N<>N
<- nat`ne-anti-reflexive N<>N F
<- false-implies-not-member F F1.
%worlds () (update-preserves-not-member-converse-helper _ _ _ _ _).
%total { } (update-preserves-not-member-converse-helper _ _ _ _ _).
- : update-preserves-not-member-converse F2 U F1
<- member?-total D
<- nat`eq?-total E
<- update-preserves-not-member-converse-helper F2 U D E F1.
%worlds () (update-preserves-not-member-converse _ _ _).
%total { } (update-preserves-not-member-converse _ _ _).
%theorem update-is-cause-of-change :
forall* {M1} {N1} {N2} {M2} {D1} {D2}
forall {F:not-member M1 N1}
{U:update M1 N2 D2 M2}
{L:lookup M2 N1 D1}
exists {EN:nat`eq N1 N2} {ED:unit`eq D1 D2}
true.
%theorem update-is-cause-of-change/L :
forall* {M1} {N1} {N2} {M2} {D1} {D2} {B}
forall {F:not-member M1 N1}
{U:update M1 N2 D2 M2}
{L:lookup M2 N1 D1}
{E:nat`eq? N1 N2 B}
exists {EN:nat`eq N1 N2} {ED:unit`eq D1 D2}
true.
- : update-is-cause-of-change F U L EN ED
<- nat`eq?-total E?
<- update-is-cause-of-change/L F U L E? EN ED.
- : update-is-cause-of-change/L F U L (nat`eq?/yes) nat`eq/ ED
<- update-implies-lookup U L'
<- lookup-deterministic L L' eq/ nat`eq/ ED.
- : update-is-cause-of-change/L F U L (nat`eq?/no N1<>N2) EN ED
<- update-preserves-not-member F U N1<>N2 F'
<- not-member-lookup-not-equal F' L N1<>N1
<- nat`ne-anti-reflexive N1<>N1 V
<- nat`false-implies-eq V EN
<- unit`false-implies-eq V ED.
%worlds () (update-is-cause-of-change/L _ _ _ _ _ _).
%total { } (update-is-cause-of-change/L _ _ _ _ _ _).
%worlds () (update-is-cause-of-change _ _ _ _ _).
%total { } (update-is-cause-of-change _ _ _ _ _).
%theorem update-preserves-membership :
forall* {M1} {N1} {B} {N2} {D} {M2}
forall {MD1:member? M1 N1 B} {U:update M1 N2 D M2} {N:nat`ne N1 N2}
exists {MD2:member? M2 N1 B}
true.
- : update-preserves-membership (member?/in L) U NE (member?/in L')
<- update-preserves-lookup L U NE L'.
- : update-preserves-membership (member?/out F) U NE (member?/out F')
<- update-preserves-not-member F U NE F'.
%worlds () (update-preserves-membership _ _ _ _).
%total {} (update-preserves-membership _ _ _ _).
%theorem update-preserves-membership-converse :
forall* {M1} {N1} {B} {N2} {D} {M2}
forall {MD2:member? M2 N1 B} {U:update M1 N2 D M2} {N:nat`ne N1 N2}
exists {MD1:member? M1 N1 B}
true.
- : update-preserves-membership-converse (member?/in L2) U NE (member?/in L1)
<- update-preserves-lookup-converse L2 U NE L1.
- : update-preserves-membership-converse (member?/out F2) U NE (member?/out F1)
<- update-preserves-not-member-converse F2 U F1.
%worlds () (update-preserves-membership-converse _ _ _ _).
%total { } (update-preserves-membership-converse _ _ _ _).
%theorem lookup-update-preserves-membership :
forall* {M1} {N1} {B} {N2} {D1} {D2} {M2}
forall {MD1:member? M1 N1 B} {L:lookup M1 N2 D1} {U:update M1 N2 D2 M2}
exists {MD2:member? M2 N1 B}
true.
%theorem lookup-update-preserves-membership/L :
forall* {M1} {N1} {B} {N2} {D1} {D2} {M2} {B2}
forall {MD1:member? M1 N1 B} {L:lookup M1 N2 D1} {U:update M1 N2 D2 M2}
{EQ?:nat`eq? N1 N2 B2}
exists {MD2:member? M2 N1 B}
true.
- : lookup-update-preserves-membership/L MD1 _ Ux1 (nat`eq?/no N1<>N2) MD2
<- update-preserves-membership MD1 Ux1 N1<>N2 MD2.
- : lookup-update-preserves-membership/L
(member?/in _) _ U (nat`eq?/yes) (member?/in L2)
<- update-implies-lookup U L2.
- : lookup-update-preserves-membership/L
(member?/out F1) L1 _ nat`eq?/yes (member?/out F2)
<- not-member-lookup-not-equal F1 L1 NE
<- nat`ne-anti-reflexive NE F
<- false-implies-not-member F F2.
%worlds () (lookup-update-preserves-membership/L _ _ _ _ _).
%total { } (lookup-update-preserves-membership/L _ _ _ _ _).
- : lookup-update-preserves-membership MD1 L1 U MD2
<- nat`eq?-total EQ?
<- lookup-update-preserves-membership/L MD1 L1 U EQ? MD2.
%worlds () (lookup-update-preserves-membership _ _ _ _).
%total { } (lookup-update-preserves-membership _ _ _ _).
%theorem lookup-update-preserves-membership-converse :
forall* {M1} {N1} {B} {N2} {D1} {D2} {M2}
forall {MD1:member? M2 N1 B} {L:lookup M1 N2 D1} {U:update M1 N2 D2 M2}
exists {MD2:member? M1 N1 B}
true.
- : lookup-update-preserves-membership-converse MD2 ML MU MD1
<- member?-total MD1'
<- lookup-update-preserves-membership MD1' ML MU MD2'
<- member?-deterministic MD2' MD2 eq/ nat`eq/ B'=B
<- member?-respects-eq MD1' eq/ nat`eq/ B'=B MD1.
%worlds () (lookup-update-preserves-membership-converse _ _ _ _).
%total { } (lookup-update-preserves-membership-converse _ _ _ _).
%theorem update-preserves-in-member :
forall* {M1} {N1} {N2} {D} {M2}
forall {MD1:member? M1 N1 true} {U:update M1 N2 D M2}
exists {MD2:member? M2 N1 true}
true.
%theorem update-preserves-in-member/L :
forall* {M1} {N1} {N2} {D} {M2} {B}
forall {MD1:member? M1 N1 true} {U:update M1 N2 D M2}
{E: nat`eq? N1 N2 B}
exists {MD2:member? M2 N1 true}
true.
- : update-preserves-in-member/L
(member?/in ML1) U (nat`eq?/no N1<>N2) (member?/in ML2)
<- update-preserves-lookup ML1 U N1<>N2 ML2.
- : update-preserves-in-member/L _ U (nat`eq?/yes) (member?/in ML)
<- update-implies-lookup U ML.
%worlds () (update-preserves-in-member/L _ _ _ _).
%total { } (update-preserves-in-member/L _ _ _ _).
- : update-preserves-in-member MD1 U MD2
<- nat`eq?-total E
<- update-preserves-in-member/L MD1 U E MD2.
%worlds () (update-preserves-in-member _ _ _).
%total { } (update-preserves-in-member _ _ _).
%theorem update-overwrites :
forall* {M1} {N1} {D1} {M2} {N2} {D2} {M3}
forall {U1:update M1 N1 D1 M2} {U2:update M2 N2 D2 M3}
{E:nat`eq N1 N2}
exists {U12:update M1 N1 D2 M3}
true.
- : update-overwrites (update/0) (update/= nat`eq/) nat`eq/ (update/0).
- : update-overwrites (update/= nat`eq/) (update/= nat`eq/) nat`eq/ (update/= nat`eq/).
- : update-overwrites (update/< P) (update/= nat`eq/) nat`eq/ (update/< P).
- : update-overwrites (update/> U1 P) (update/> U2 P') nat`eq/ (update/> U3 P)
<- plus-right-cancels P P' nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0'
<- update-overwrites U1 U2 N0=N0' U3.
%% contradiction cases
- : update-overwrites (update/0) (update/< N3+1+N=N) nat`eq/ U
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/0) (update/> _ N0+1+N=N) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/= nat`eq/) (update/< N3+1+N=N) nat`eq/ U
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/= nat`eq/) (update/> _ N0+1+N=N) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/< _) (update/< N3+1+N=N) nat`eq/ U
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/< _) (update/> _ N0+1+N=N) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/> _ N0+1+N=N) (update/= nat`eq/) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/> _ N0+1+N1=N2) (update/< N3+1+N2=N1) nat`eq/ U
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-update F U.
%worlds () (update-overwrites M1^N1=D1->M2 M2^N2=D2->M3 N1=N2
%{=>}% M1^N1=D2->M3).
%total (U) (update-overwrites U _ _ _).
%theorem update-overwrites-converse :
forall* {M1} {N1} {D1} {M2} {D2} {M3}
forall {U12:update M1 N1 D1 M3} {U1:update M1 N1 D2 M2}
exists {U2:update M2 N1 D1 M3}
true.
- : update-overwrites-converse U12 U1 U2
<- update-total U2P
<- update-overwrites U1 U2P nat`eq/ U12P
<- update-deterministic U12P U12 eq/ nat`eq/ unit`eq/ M2P=M2
<- update-respects-eq U2P eq/ nat`eq/ unit`eq/ M2P=M2 U2.
%worlds () (update-overwrites-converse _ _ _).
%total { } (update-overwrites-converse _ _ _).
%theorem update-may-have-no-effect :
forall* {M1} {N} {D} {M2}
forall {L:lookup M1 N D} {U:update M1 N D M2}
exists {E:eq M1 M2}
true.
- : update-may-have-no-effect (lookup/= nat`eq/) U E
<- update/=-inversion U nat`eq/ E.
- : update-may-have-no-effect (lookup/> L1 N0+1+N1=N2) U E
<- update/>-inversion U N0+1+N1=N2 _ U1 M112=M2
<- update-may-have-no-effect L1 U1 M1=M2
<- map/+-preserves-eq nat`eq/ unit`eq/ M1=M2 M111=M112
<- eq-transitive M111=M112 M112=M2 E.
%worlds () (update-may-have-no-effect _ _ _).
%total (L) (update-may-have-no-effect L _ _).
%theorem update-idempotent :
forall* {M1} {N1} {D1} {M2} {N2} {D2} {M3}
forall {U1:update M1 N1 D1 M2} {U2:update M2 N2 D2 M3}
{EN:nat`eq N1 N2} {ED:unit`eq D1 D2}
exists {EM:eq M2 M3}
true.
- : update-idempotent U1 U2 nat`eq/ unit`eq/ M2=M3
<- update-overwrites U1 U2 nat`eq/ M1^N=D->M3
<- update-deterministic U1 M1^N=D->M3 eq/ nat`eq/ unit`eq/ M2=M3.
%worlds () (update-idempotent M1^N1=D1->M2 M2^N2=D2->M3 N1=N2 D1=D2
%{=>}% M2=M3).
%total {} (update-idempotent _ _ _ _ _).
%theorem update-commutes :
forall* {M} {N1} {D1} {M1} {N2} {D2} {M12}
forall {U1:update M N1 D1 M1} {U12:update M1 N2 D2 M12}
{NE:nat`ne N1 N2}
exists {M2} {U2:update M N2 D2 M2} {U21:update M2 N1 D1 M12}
true.
- : update-commutes update/0 (update/= nat`eq/) N<>N map/0 U2 U21
<- nat`ne-anti-reflexive N<>N F
<- false-implies-update F U2
<- false-implies-update F U21.
- : update-commutes update/0 (update/< N'+1+N2=N1) _ _ update/0
(update/> update/0 N'+1+N2=N1).
- : update-commutes update/0 (update/> update/0 N'+1+N1=N2) _ _ update/0
(update/< N'+1+N1=N2).
- : update-commutes (update/= nat`eq/) (update/= nat`eq/) N<>N map/0 U2 U21
<- nat`ne-anti-reflexive N<>N F
<- false-implies-update F U2
<- false-implies-update F U21.
- : update-commutes (update/= nat`eq/) (update/< N'+1+N2=N1) _ _
(update/< N'+1+N2=N1) (update/> (update/= nat`eq/) N'+1+N2=N1).
- : update-commutes (update/= nat`eq/) (update/> U N'+1+N1=N2) _ _
(update/> U N'+1+N1=N2) (update/= nat`eq/).
- : update-commutes (update/< _) (update/= nat`eq/) N<>N map/0 U2 U21
<- nat`ne-anti-reflexive N<>N F
<- false-implies-update F U2
<- false-implies-update F U21.
- : update-commutes (update/< N1'+1+N1=N) (update/< N2'+1+N2=N1) _ _
(update/< N2''+1+N2=N)
(update/> (update/< N1'+1+N2'=N2'') N2'+1+N2=N1)
<- plus-swap-succ N2'+1+N2=N1 N2'+N2+1=N1
<- plus-associative-converse N2'+N2+1=N1 N1'+1+N1=N
N2'' N1'+1+N2'=N2'' N2''+N2+1=N
<- plus-swap-succ-converse N2''+N2+1=N N2''+1+N2=N.
- : update-commutes ((update/< N11+1+N1=N):update (map/+ N D M) _ _ _)
(update/> (update/= nat`eq/) N11+1+N1=N2) _
(map/+ N2 D2 M)
(update/= N=N2)
((update/< N11+1+N1=N2):update _ N1 D1 _)
<- plus-deterministic N11+1+N1=N N11+1+N1=N2 nat`eq/ nat`eq/ N=N2.
- : update-commutes (update/< N11+1+N1=N)
(update/> (update/< N2''+1+N2'=N11) N2'+1+N1=N2) _ _
(update/< N2''+1+N2=N) (update/< N2'+1+N1=N2)
<- plus-swap-succ N11+1+N1=N N11+N1+1=N
<- plus-swap-succ N2'+1+N1=N2 N2'+N1+1=N2
<- plus-associative* N2''+1+N2'=N11 N11+N1+1=N N2'+N1+1=N2
N2''+1+N2=N.
- : update-commutes (update/< N11+1+N1=N)
(update/> (update/> U N2''+1+N11=N2') N2'+1+N1=N2) _ _
(update/> U N2''+1+N=N2) (update/< N11+1+N1=N)
<- plus-swap-succ N11+1+N1=N N11+N1+1=N
<- plus-swap-succ N2'+1+N1=N2 N2'+N1+1=N2
<- plus-associative* N2''+1+N11=N2' N2'+N1+1=N2 N11+N1+1=N N2''+1+N=N2.
- : update-commutes (update/> U N11+1+N=N1) (update/= nat`eq/) _ _
(update/= nat`eq/) (update/> U N11+1+N=N1).
- : update-commutes (update/> U N11+1+N=N1) (update/< N2'+1+N2=N) _ _
(update/< N2'+1+N2=N)
(update/> (update/> U N11+1+N2'=N11') N11'+1+N2=N1)
<- plus-swap-succ N2'+1+N2=N N2'+N2+1=N
<- plus-associative-converse N2'+N2+1=N N11+1+N=N1
N11' N11+1+N2'=N11' N11'+N2+1=N1
<- plus-swap-succ-converse N11'+N2+1=N1 N11'+1+N2=N1.
- : update-commutes (update/> U1 N11+1+N=N1) (update/> U12 N2'+1+N=N2) N1<>N2
(map/+ N D M2)
(update/> U2 N2'+1+N=N2) (update/> U21 N11+1+N=N1)
<- plus-right-cancels-ne N11+1+N=N1 N2'+1+N=N2 nat`eq/ N1<>N2 N11+1<>N2'+1
<- succ-preserves-ne-converse N11+1<>N2'+1 N11<>N2'
<- update-commutes U1 U12 N11<>N2' M2 U2 U21.
%worlds () (update-commutes M^N1=D1->M1 M1^D2=N2->M12 N1<>N2
%{=>}% M2 M^N2=D2->M2 M2^N1=D1->M12).
%total (U1) (update-commutes U1 _ _ _ _ _).
%theorem update-commutes* :
forall* {M} {N1} {D1} {M1} {N2} {D2} {M12} {M2}
forall {U1:update M N1 D1 M1} {U12:update M1 N2 D2 M12}
{NE:nat`ne N1 N2} {U2:update M N2 D2 M2}
exists {U21:update M2 N1 D1 M12}
true.
- : update-commutes* M^N1=D1->M1 M1^D2=N2->M12 N1<>N2 M^N2=D2->M2 M2^N1=D1->M12
<- update-commutes M^N1=D1->M1 M1^D2=N2->M12 N1<>N2
M2' M^N2=D2->M2' M2'^N1=D1->M12
<- update-deterministic M^N2=D2->M2' M^N2=D2->M2 eq/ nat`eq/
unit`eq/ M2'=M2
<- update-respects-eq M2'^N1=D1->M12 M2'=M2 nat`eq/
unit`eq/ eq/ M2^N1=D1->M12.
%worlds () (update-commutes* M^N1=D1->M1 M1^D2=N2->M12 N1<>N2 M^N2=D2->M2
%{=>}% M2^N1=D1->M12).
%total {} (update-commutes* _ _ _ _ _).
%% The following theorem is needed if you want to iteratively
%% do something with a set. It says that you can take out an element
%% and (using the update-preserves-X-converse theorems) get a smaller set
%% that differs only for this element:
%theorem can-remove :
forall* {M} {S} {N} {D}
forall {SZ:size M S} {L:lookup M N D}
exists {M-} {S-} {SZ-:size M- S-} {E:nat`eq (s S-) S}
{U:update M- N D M} {F:not-member M- N}
true.
- : can-remove (size/+ _) (lookup/= _) _ _ size/0 nat`eq/ update/0 not-member/0.
- : can-remove (size/+ (size/+ SZ)) (lookup/= nat`eq/) _ _ (size/+ SZ) nat`eq/
(update/< N3+1+N2=N1) (not-member/< N1>N2)
<- plus-total N3+1+N2=N1
<- plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2.
- : can-remove (size/+ SZ) (lookup/> LK N0+1+N1=N2) _ _
(size/+ SZ2) E
(update/> U2 N0+1+N1=N2) (not-member/> F2 N0+1+N1=N2)
<- can-remove SZ LK M- S- SZ2 E2 U2 F2
<- succ-deterministic E2 E.
%worlds () (can-remove _ _ _ _ _ _ _ _).
%total (L) (can-remove _ L _ _ _ _ _ _).
%%%% Map comparison
%%% Definition of leq
leq : map -> map -> type.
leq/0 : leq map/0 M.
leq/= : leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`eq N1 N2
<- unit`leq D1 D2
<- leq M1 M2.
leq/> : leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`plus (s N3) N2 N1
<- leq (map/+ N3 D1 M1) M2.
%%% Theorems about leq
%theorem false-implies-leq :
forall* {M1} {M2}
forall {F:void}
exists {L:leq M1 M2}
true.
%worlds () (false-implies-leq _ _).
%total {} (false-implies-leq _ _).
%theorem leq-respects-eq :
forall* {M1} {M2} {M1'} {M2'}
forall {L:leq M1 M2} {E1:eq M1 M1'} {E2:eq M2 M2'}
exists {LP:leq M1' M2'}
true.
- : leq-respects-eq L eq/ eq/ L.
%worlds () (leq-respects-eq _ _ _ _).
%total {} (leq-respects-eq _ _ _ _).
%reduces L1 = L2 (leq-respects-eq L1 _ _ L2).
%theorem leq/0-inversion :
forall* {M1} {M2}
forall {L:leq M1 M2} {E2:eq M2 map/0}
exists {E1:eq M1 map/0}
true.
- : leq/0-inversion leq/0 eq/ eq/.
%worlds () (leq/0-inversion _ _ _).
%total { } (leq/0-inversion _ _ _).
%theorem leq/=-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2}
forall {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)} {EN:nat`eq N1 N2}
exists {ED:unit`leq D1 D2} {EM:leq M1 M2}
true.
- : leq/=-inversion (leq/= M1<=M2 D1<=D2 nat`eq/) nat`eq/ D1<=D2 M1<=M2.
- : leq/=-inversion (leq/> M311<=M2 N3+1+N=N) nat`eq/ ED M1<=M2
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- unit`false-implies-leq F ED
<- false-implies-eq F M311=M1
<- leq-respects-eq M311<=M2 M311=M1 eq/ M1<=M2.
%worlds () (leq/=-inversion _ _ _ _).
%total { } (leq/=-inversion _ _ _ _).
%reduces L1 < L (leq/=-inversion L _ _ L1).
%theorem leq/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3}
forall {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N3) N2 N1}
exists {EM:leq (map/+ N3 D1 M1) M2}
true.
- : leq/>-inversion (leq/= M1<=M2 D1<=D2 nat`eq/) N3+1+N=N M311<=M2
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F M1=M311
<- leq-respects-eq M1<=M2 M1=M311 eq/ M311<=M2.
- : leq/>-inversion (leq/> M311'<=M2 N3P+1+N2=N1) N3+1+N2=N1 M311<=M2
<- plus-right-cancels N3P+1+N2=N1 N3+1+N2=N1 nat`eq/ nat`eq/ N3P+1=N3+1
<- succ-cancels N3P+1=N3+1 N3P=N3
<- map/+-preserves-eq N3P=N3 unit`eq/ eq/ M311'=M311
<- leq-respects-eq M311'<=M2 M311'=M311 eq/ M311<=M2.
%worlds () (leq/>-inversion _ _ _).
%total { } (leq/>-inversion _ _ _).
%reduces LP < L (leq/>-inversion L _ LP).
%theorem leq-contradiction :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0}
forall {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N0) N1 N2}
exists {F:void}
true.
- : leq-contradiction (leq/= _ _ nat`eq/) N0+1+N=N F
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F.
- : leq-contradiction (leq/> _ N3+1+N2=N1) N0+1+N1=N2 F
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F.
%worlds () (leq-contradiction _ _ _).
%total { } (leq-contradiction _ _ _).
%theorem leq-reflexive :
forall {M}
exists {L:leq M M}
true.
- : leq-reflexive map/0 leq/0.
- : leq-reflexive (map/+ N D M) (leq/= M<=M D<=D nat`eq/)
<- unit`leq-reflexive D D<=D
<- leq-reflexive M M<=M.
%worlds () (leq-reflexive _ _).
%total (M) (leq-reflexive M _).
%theorem leq-anti-symmetric :
forall* {M1} {M2}
forall {L1: leq M1 M2} {L2:leq M2 M1}
exists {E: eq M1 M2}
true.
- : leq-anti-symmetric leq/0 leq/0 eq/.
- : leq-anti-symmetric (leq/= M1<=M2 D1<=D2 nat`eq/)
(leq/= M2<=M1 D2<=D1 nat`eq/) E
<- unit`leq-anti-symmetric D1<=D2 D2<=D1 D1=D2
<- leq-anti-symmetric M1<=M2 M2<=M1 M1=M2
<- map/+-preserves-eq nat`eq/ D1=D2 M1=M2 E.
- : leq-anti-symmetric (leq/= _ _ nat`eq/) (leq/> _ N3+1+N=N) E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : leq-anti-symmetric (leq/> _ N3+1+N=N) (leq/= _ _ nat`eq/) E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : leq-anti-symmetric (leq/> _ N3+1+N2=N1) (leq/> _ N0+1+N1=N2) E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (leq-anti-symmetric _ _ _).
%total (L) (leq-anti-symmetric L _ _).
%theorem leq-transitive :
forall* {M1} {M2} {M3}
forall {L1:leq M1 M2} {L2:leq M2 M3}
exists {L3:leq M1 M3}
true.
- : leq-transitive leq/0 _ leq/0.
- : leq-transitive (leq/= M1<=M2 D1<=D2 nat`eq/) (leq/= M2<=M3 D2<=D3 nat`eq/)
(leq/= M1<=M3 D1<=D3 nat`eq/)
<- unit`leq-transitive D1<=D2 D2<=D3 D1<=D3
<- leq-transitive M1<=M2 M2<=M3 M1<=M3.
- : leq-transitive (leq/= M1<=M2 D1<=D2 nat`eq/) (leq/> M522<=M3 N5+1+N3=N2)
(leq/> M511<=M3 N5+1+N3=N2)
<- leq-transitive (leq/= M1<=M2 D1<=D2 nat`eq/) M522<=M3 M511<=M3.
- : leq-transitive (leq/> M011<=M2 N0+1+N=N1) (leq/= M2<=M3 D2<=D3 nat`eq/)
(leq/> M011<=M3 N0+1+N=N1)
<- leq-transitive M011<=M2 M2<=M3 M011<=M3.
- : leq-transitive (leq/> M011<=M2 N0+1+N2=N1) (leq/> M522<=M3 N5+1+N3=N2)
(leq/> M411<=M3 N4+1+N3=N1)
<- nat`plus-swap-succ N5+1+N3=N2 N5+N3+1=N2
<- nat`plus-associative-converse N5+N3+1=N2 N0+1+N2=N1 N4 N0+1+N5=N4
N4+N3+1=N1
<- nat`plus-swap-succ-converse N4+N3+1=N1 N4+1+N3=N1
<- leq-transitive (leq/> M011<=M2 N0+1+N5=N4) M522<=M3 M411<=M3.
%worlds () (leq-transitive _ _ _).
%total (L) (leq-transitive _ L _).
%theorem map/+-preserves-leq :
forall* {N1} {N2} {D1} {D2} {M1} {M2}
forall {E:nat`eq N1 N2} {LD:unit`leq D1 D2} {LM:leq M1 M2}
exists {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
true.
- : map/+-preserves-leq N1=N2 D1<=D2 M1<=M2 (leq/= M1<=M2 D1<=D2 N1=N2).
%worlds () (map/+-preserves-leq _ _ _ _).
%total { } (map/+-preserves-leq _ _ _ _).
%theorem lookup-respects-leq :
forall* {M} {N} {D} {MP}
forall {L:lookup M N D} {ME:leq M MP}
exists {DP} {L:lookup MP N DP} {DE:unit`leq D DP}
true.
- : lookup-respects-leq (lookup/= nat`eq/) (leq/= _ D1<=D2 nat`eq/)
_ (lookup/= nat`eq/) D1<=D2.
- : lookup-respects-leq (lookup/= nat`eq/) (leq/> M311<=M2 N3+1+N2=N1)
D2 (lookup/> L13 N3+1+N2=N1) D1<=D2
<- lookup-respects-leq (lookup/= nat`eq/) M311<=M2 D2 L13 D1<=D2.
- : lookup-respects-leq (lookup/> L13 N3+1+N2=N1) (leq/= M1<=M2 _ nat`eq/)
D2 (lookup/> L13' N3+1+N2=N1) D1<=D2
<- lookup-respects-leq L13 M1<=M2 D2 L13' D1<=D2.
- : lookup-respects-leq (lookup/> L10 N0+1+N1=N) (leq/> M311<=M2 N3+1+N2=N1)
D2 (lookup/> L14' N4+1+N2=N) D1<=D2
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- nat`plus-associative-converse N3+N2+1=N1 N0+1+N1=N
N4 N0+1+N3=N4 N4+N2+1=N
<- nat`plus-swap-succ-converse N4+N2+1=N N4+1+N2=N
<- lookup-respects-leq (lookup/> L10 N0+1+N3=N4) M311<=M2 D2 L14' D1<=D2.
%worlds () (lookup-respects-leq _ _ _ _ _).
%total (L) (lookup-respects-leq _ L _ _ _).
%theorem not-member-respects-geq :
forall* {M} {MP} {N}
forall {FP:not-member MP N} {L:leq M MP}
exists {F:not-member M N}
true.
- : not-member-respects-geq F leq/0 not-member/0.
- : not-member-respects-geq (not-member/< R) (leq/= _ _ nat`eq/) (not-member/< R).
- : not-member-respects-geq (not-member/< N2>N) (leq/> _ N3+1+N2=N1) (not-member/< N1>N)
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- gt-transitive N1>N2 N2>N N1>N.
- : not-member-respects-geq (not-member/> F20 N0+1+N2=N) (leq/= M1<=M2 _ nat`eq/)
(not-member/> F10 N0+1+N2=N)
<- not-member-respects-geq F20 M1<=M2 F10.
- : {F3110:not-member (map/+ N3 D1 M1) N0}
{N0+1+N2=N:plus (s N0) N2 N}
{N3+1+N2=N1:plus (s N3) N2 N1}
not-member-respects-geq
(not-member/> F20 N0+1+N2=N: not-member (map/+ N2 D2 M2) N)
(leq/> M311<=M2 N3+1+N2=N1) F'
<- not-member-respects-geq F20 M311<=M2 F3110
<- nat`plus-swap-succ N0+1+N2=N N0+N2+1=N
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-right-preserves-not-member* F3110 N3+N2+1=N1 N0+N2+1=N F'.
%worlds () (not-member-respects-geq _ _ _).
%total (F) (not-member-respects-geq F _ _).
%theorem leq-implies-size-le:
forall* {M1} {M2} {N1} {N2}
forall {L:leq M1 M2} {SZ1:size M1 N1} {SZ2:size M2 N2}
exists {G:ge N2 N1}
true.
- : leq-implies-size-le leq/0 size/0 N2=|M2| N2>=0
<- plus-commutative (plus/z:plus z N2 N2) N2+0=N2
<- plus-implies-ge N2+0=N2 N2>=0.
- : leq-implies-size-le (leq/= M1<=M2 _ _) (size/+ N1=|M1|) (size/+ N2=|M2|)
N2+1>=N1+1
<- leq-implies-size-le M1<=M2 N1=|M1| N2=|M2| N2>=N1
<- succ-preserves-ge N2>=N1 N2+1>=N1+1.
- : leq-implies-size-le (leq/> M311<=M2 _) (size/+ N1=|M1|) (size/+ N2=|M2|)
(ge/> N2+1>N1+1)
<- leq-implies-size-le M311<=M2 (size/+ N1=|M1|) N2=|M2| N2>=N1+1
<- succ-implies-gt nat`eq/ N2+1>N2
<- gt-transitive-ge N2+1>N2 N2>=N1+1 N2+1>N1+1.
%worlds () (leq-implies-size-le _ _ _ _).
%total (L) (leq-implies-size-le L _ _ _).
%theorem leq-implies-bound-le:
forall* {M1} {M2} {N1} {N2}
forall {L:leq M1 M2} {BD1:bound M1 N1} {BD2:bound M2 N2}
exists {G:ge N2 N1}
true.
- : leq-implies-bound-le leq/0 bound/0 _ N2>=0
<- plus-commutative plus/z N2+0=N2
<- plus-implies-ge N2+0=N2 N2>=0.
- : leq-implies-bound-le (leq/= M1<=M2 _ nat`eq/)
(bound/+ N+1+N1=N3 DM1=N3
<- leq-implies-bound-le M1<=M2 DM1=N1
<- plus-left-preserves-ge* N2>=N1 N+1+N2=N4 N+1+N1=N3 N4>=N3.
- : leq-implies-bound-le (leq/> M311<=M2 N3+1+N2=N1)
(bound/+ N1+1+N10=N11 DM1=N11
<- plus-total N3+1+N10=N13
<- leq-implies-bound-le M311<=M2 (bound/+ N3+1+N10=N13 DM1=N13
<- plus-swap-succ N1+1+N10=N11 N1+N10+1=N11
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-commutative N3+N2+1=N1 N2+1+N3=N1
<- plus-swap-succ N3+1+N10=N13 N3+N10+1=N13
<- plus-associative* N2+1+N3=N1 N1+N10+1=N11 N3+N10+1=N13 N2+1+N13=N11
<- plus-left-preserves-ge* N20>=N13 N2+1+N20=N22 N2+1+N13=N11 N22>=N11.
%worlds () (leq-implies-bound-le _ _ _ _).
%total (L) (leq-implies-bound-le L _ _ _).
%theorem shift-left-preserves-leq*:
forall* {M1} {M2} {N} {SM1} {D}
forall {L:leq M1 M2}
{S1:shift N M1 SM1}
exists {SL:leq SM1 (map/+ N D M2)}
true.
- : shift-left-preserves-leq* _ shift/0 leq/0.
- : shift-left-preserves-leq* M111<=M2 (shift/+ N+1+N1=N1')
(leq/> M111<=M2 N1+1+N=N1')
<- plus-swap-succ N+1+N1=N1' N+N1+1=N1'
<- plus-commutative N+N1+1=N1' N1+1+N=N1'.
%worlds () (shift-left-preserves-leq* _ _ _).
%total { } (shift-left-preserves-leq* _ _ _).
%theorem shift-preserves-leq*:
forall* {M1} {M2} {N} {SM1} {SM2}
forall {L:leq M1 M2}
{S1:shift N M1 SM1}
{S1:shift N M2 SM2}
exists {SL:leq SM1 SM2}
true.
- : shift-preserves-leq* _ shift/0 _ leq/0.
- : shift-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(shift/+ N+1+N1=N1')
(shift/+ N+1+N1=N2')
(leq/= M1<=M2 D1<=D2 N1'=N2')
<- plus-deterministic N+1+N1=N1' N+1+N1=N2' nat`eq/ nat`eq/ N1'=N2'.
- : shift-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(shift/+ N+1+N1=N1')
(shift/+ N+1+N2=N2')
(leq/> M311<=M2 N3+1+N2'=N1')
<- plus-commutative N3+1+N2=N1 N2+N3+1=N1
<- plus-associative-converse* N2+N3+1=N1 N+1+N1=N1' N+1+N2=N2' N2'+N3+1=N1'
<- plus-commutative N2'+N3+1=N1' N3+1+N2'=N1'.
%worlds () (shift-preserves-leq* _ _ _ _).
%total { } (shift-preserves-leq* _ _ _ _).
%theorem update-left-preserves-leq*:
forall* {M1} {M2} {N} {D} {M1'} {M2'}
forall {L:leq M1 M2}
{U1:update M1 N D M1'}
{U2:update M2 N D M2'}
exists {LP:leq M1' M2'}
true.
- : update-left-preserves-leq* leq/0 update/0 update/0 (leq/= leq/0 D<=D nat`eq/)
<- unit`leq-reflexive _ D<=D.
- : update-left-preserves-leq* leq/0 update/0 (update/= nat`eq/)
(leq/= leq/0 D<=D nat`eq/)
<- unit`leq-reflexive _ D<=D.
- : update-left-preserves-leq* leq/0 update/0 (update/< _)
(leq/= leq/0 D<=D nat`eq/)
<- unit`leq-reflexive _ D<=D.
- : update-left-preserves-leq* leq/0 update/0 (update/> U2505 N5+1+N2=N)
(leq/> M500<=M5 N5+1+N2=N)
<- update-left-preserves-leq* leq/0 update/0 U2505 M500<=M5.
- : update-left-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(update/= nat`eq/)
(U2:update (map/+ N D2 M2) N D M)
M001<=M
<- update/=-inversion U2 nat`eq/ M002=M
<- unit`leq-reflexive _ D<=D
<- leq-respects-eq (leq/= M1<=M2 D<=D nat`eq/) eq/ M002=M M001<=M.
- : update-left-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(update/< N3+1+N=N1)
(U2:update (map/+ N1 D2 M2) N D M)
M00M311<=M
<- update/<-inversion U2 N3+1+N=N1 M00M322=M
<- unit`leq-reflexive _ D<=D
<- leq-respects-eq (leq/= (leq/= M1<=M2 D1<=D2 nat`eq/) D<=D nat`eq/) eq/
M00M322=M M00M311<=M.
- : update-left-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(update/> U1303 N3+1+N1=N)
(U2:update (map/+ N1 D2 M2) N D M)
M113<=M
<- update/>-inversion U2 N3+1+N1=N M4 U2304 M124=M
<- update-left-preserves-leq* M1<=M2 U1303 U2304 M3<=M4
<- leq-respects-eq (leq/= M3<=M4 D1<=D2 nat`eq/) eq/ M124=M M113<=M.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/= nat`eq/)
(U2:update (map/+ N2 D2 M2) N1 D M)
M101<=M
<- update/>-inversion U2 N3+1+N2=N1 M4 U2304 M224=M
<- update-left-preserves-leq* M311<=M2 (update/= nat`eq/) U2304 M301<=M4
<- leq-respects-eq (leq/> M301<=M4 N3+1+N2=N1) eq/ M224=M M101<=M.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N=N1)
(update/< N4+1+N=N1)
(update/= nat`eq/) %% hence N=N2
(leq/= M411<=M2 D<=D nat`eq/)
<- nat`plus-right-cancels N3+1+N=N1 N4+1+N=N1 nat`eq/ nat`eq/ N3+1=N4+1
<- nat`succ-cancels N3+1=N4+1 N3=N4
<- map/+-preserves-eq N3=N4 unit`eq/ eq/ M311=M411
<- leq-respects-eq M311<=M2 M311=M411 eq/ M411<=M2
<- unit`leq-reflexive _ D<=D.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/< N4+1+N=N1)
(update/< N5+1+N=N2)
(leq/= (leq/> M311<=M2 N3+1+N5=N4) D<=D nat`eq/)
<- nat`plus-swap-succ N5+1+N=N2 N5+N+1=N2
<- nat`plus-associative-converse N5+N+1=N2 N3+1+N2=N1
N4' N3+1+N5=N4' N4'+N+1=N1
<- nat`plus-swap-succ N4+1+N=N1 N4+N+1=N1
<- nat`plus-right-cancels N4'+N+1=N1 N4+N+1=N1 nat`eq/ nat`eq/ N4'=N4
<- nat`plus-respects-eq N3+1+N5=N4' nat`eq/ nat`eq/ N4'=N4 N3+1+N5=N4
<- unit`leq-reflexive _ D<=D.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/< N4+1+N=N1)
(update/> U2505 N5+1+N2=N)
(leq/> M50M411<=M5 N5+1+N2=N)
<- nat`plus-swap-succ N5+1+N2=N N5+N2+1=N
<- nat`plus-associative-converse N5+N2+1=N N4+1+N=N1
N3P N4+1+N5=N3P N3P+N2+1=N1
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- nat`plus-right-cancels N3P+N2+1=N1 N3+N2+1=N1 nat`eq/ nat`eq/ N3P=N3
<- nat`plus-respects-eq N4+1+N5=N3P nat`eq/ nat`eq/ N3P=N3 N4+1+N5=N3
<- update-left-preserves-leq* M311<=M2 (update/< N4+1+N5=N3) U2505
M50M411<=M5.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/> U1404 N4+1+N1=N)
(U2:update (map/+ N2 D2 M2) N D M)
M114<=M
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- nat`plus-associative-converse N3+N2+1=N1 N4+1+N1=N
N5 N4+1+N3=N5 N5+N2+1=N
<- nat`plus-swap-succ-converse N5+N2+1=N N5+1+N2=N
<- update/>-inversion U2 N5+1+N2=N M5 U2505 M225=M
<- update-left-preserves-leq* M311<=M2 (update/> U1404 N4+1+N3=N5) U2505
M314<=M5
<- leq-respects-eq (leq/> M314<=M5 N3+1+N2=N1) eq/ M225=M M114<=M.
%worlds () (update-left-preserves-leq* _ _ _ _).
%total (U) (update-left-preserves-leq* _ _ U _).
%theorem update-right-preserves-leq*:
forall* {M} {N} {D1} {D2} {M1'} {M2'}
forall {L:unit`leq D1 D2}
{U1:update M N D1 M1'}
{U2:update M N D2 M2'}
exists {LP:leq M1' M2'}
true.
- : update-right-preserves-leq* D1<=D2 update/0 update/0
(leq/= leq/0 D1<=D2 nat`eq/).
- : update-right-preserves-leq* D1<=D2 (update/= nat`eq/) U2 L
<- update/=-inversion U2 nat`eq/ M221=M2'
<- leq-reflexive _ M1<=M1
<- leq-respects-eq (leq/= M1<=M1 D1<=D2 nat`eq/) eq/ M221=M2' L.
- : update-right-preserves-leq* D1<=D2 (update/< P) U2 L
<- update/<-inversion U2 P M22311=M2'
<- leq-reflexive _ M311<=M311
<- leq-respects-eq (leq/= M311<=M311 D1<=D2 nat`eq/) eq/ M22311=M2' L.
- : update-right-preserves-leq* D1<=D2 (update/> U1 P) U22 L
<- update/>-inversion U22 P M2' U2 M112=M
<- update-right-preserves-leq* D1<=D2 U1 U2 M1'<=M2'
<- unit`leq-reflexive _ D<=D
<- leq-respects-eq (leq/= M1'<=M2' D<=D nat`eq/) eq/ M112=M L.
%worlds () (update-right-preserves-leq* _ _ _ _).
%total (U) (update-right-preserves-leq* _ U _ _).
%theorem update-preserves-leq* :
forall* {M1} {M2} {N} {D1} {D2} {M1'} {M2'}
forall {L:leq M1 M2} {L:unit`leq D1 D2}
{U1:update M1 N D1 M1'}
{U2:update M2 N D2 M2'}
exists {LP:leq M1' M2'}
true.
- : update-preserves-leq* M1<=M2 D1<=D2 M1^N=D1->M1' M2^N=D2->M2' M1'<=M2'
<- update-total M2^N=D1->MM
<- update-left-preserves-leq* M1<=M2 M1^N=D1->M1' M2^N=D1->MM M1'<=MM
<- update-right-preserves-leq* D1<=D2 M2^N=D1->MM M2^N=D2->M2' MM<=M2'
<- leq-transitive M1'<=MM MM<=M2' M1'<=M2'.
%worlds () (update-preserves-leq* _ _ _ _ _).
%total { } (update-preserves-leq* _ _ _ _ _).
%theorem not-member-update-implies-leq :
forall* {M1} {N} {D} {M2}
forall {F:not-member M1 N} {U:update M1 N D M2}
exists {L:leq M1 M2}
true.
- : not-member-update-implies-leq not-member/0 U leq/0.
- : not-member-update-implies-leq (not-member/< N2 M311<=M311 N3+1+N2=N1) eq/ M22311=M2 L.
- : not-member-update-implies-leq (not-member/> F1 N0+1+N1=N2) U L
<- update/>-inversion U N0+1+N1=N2 _ U1 M112=M
<- not-member-update-implies-leq F1 U1 L1
<- unit`leq-reflexive _ DL
<- leq-respects-eq (leq/= L1 DL nat`eq/) eq/ M112=M L.
%worlds () (not-member-update-implies-leq _ _ _).
%total (F) (not-member-update-implies-leq F _ _).
%theorem lookup-update-preserves-leq :
forall* {M1} {N} {D1} {D2} {M2}
forall {L:lookup M1 N D1} {U:update M1 N D2 M2}
{L:unit`leq D1 D2}
exists {L:leq M1 M2}
true.
- : lookup-update-preserves-leq (lookup/= nat`eq/) U D1<=D2 L
<- update/=-inversion U nat`eq/ M221=M2
<- leq-reflexive _ M1<=M1
<- leq-respects-eq (leq/= M1<=M1 D1<=D2 nat`eq/) eq/ M221=M2 L.
- : lookup-update-preserves-leq (lookup/> L1 N0+1+N1=N2) U D1<=D2 L
<- update/>-inversion U N0+1+N1=N2 M2 U1 M112=M
<- lookup-update-preserves-leq L1 U1 D1<=D2 L1'
<- unit`leq-reflexive _ D1<=D1
<- leq-respects-eq (leq/= L1' D1<=D1 nat`eq/) eq/ M112=M L.
%worlds () (lookup-update-preserves-leq _ _ _ _).
%total (L) (lookup-update-preserves-leq L _ _ _).
%%%% Map addition
%%% Definition of union
union : map -> map -> map -> type.
union/L : union map/0 M M.
union/R : union M map/0 M.
union/= : union (map/+ N1 D1 M1) (map/+ N2 D2 M2) (map/+ N1 D3 M3)
<- nat`eq N1 N2
<- unit`union D1 D2 D3
<- union M1 M2 M3.
union/< : union (map/+ N1 D1 M1) (map/+ N2 D2 M2) (map/+ N1 D1 M3)
<- nat`plus (s N0) N1 N2
<- union M1 (map/+ N0 D2 M2) M3.
union/> : union (map/+ N1 D1 M1) (map/+ N2 D2 M2) (map/+ N2 D2 M3)
<- nat`plus (s N3) N2 N1
<- union (map/+ N3 D1 M1) M2 M3.
%%% Theorems about union
%theorem false-implies-union :
forall* {M1} {M2} {M3}
forall {F:void}
exists {D:union M1 M2 M3}
true.
%worlds () (false-implies-union _ _).
%total {} (false-implies-union _ _).
%theorem union-respects-eq :
forall* {M1} {M2} {M3} {M1P} {M2P} {M3P}
forall {A:union M1 M2 M3} {E1:eq M1 M1P} {E2:eq M2 M2P} {E3:eq M3 M3P}
exists {AP:union M1P M2P M3P}
true.
- : union-respects-eq A eq/ eq/ eq/ A.
%worlds () (union-respects-eq _ _ _ _ _).
%total {} (union-respects-eq _ _ _ _ _).
%reduces A = AP (union-respects-eq A _ _ _ AP).
%% Inversion lemmas for union
%theorem union/=-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {M}
forall {A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M}
{G:nat`eq N1 N2}
exists {D3} {M3}
{D:unit`union D1 D2 D3}
{AP:union M1 M2 M3}
{E:eq M (map/+ N1 D3 M3)}
true.
- : union/=-inversion (union/= MM DD nat`eq/) _ _ _ DD MM eq/.
- : union/=-inversion (union/< (JP:union _ (map/+ N0 D2 M2) M3) N0+1+N=N) nat`eq/
D2 M3 DJ MJ ME
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- unit`false-implies-union F DJ
<- false-implies-eq F (M022=M2:eq (map/+ N0 D2 M2) M2)
<- union-respects-eq JP eq/ M022=M2 eq/ MJ
<- false-implies-eq F ME.
- : union/=-inversion (union/> (JP:union (map/+ _ D1 M1) M2 M3) N3+1+N=N) nat`eq/
D1 M3 DJ MJ ME
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- unit`false-implies-union F DJ
<- false-implies-eq F (M311=M1:eq (map/+ N3 D1 M1) M1)
<- union-respects-eq JP M311=M1 eq/ eq/ MJ
<- false-implies-eq F ME.
%worlds () (union/=-inversion _ _ _ _ _ _ _).
%total {} (union/=-inversion _ _ _ _ _ _ _).
%reduces JP < J (union/=-inversion J _ _ _ _ JP _).
%theorem union/<-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {M} {N0}
forall {A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M}
{P:plus (s N0) N1 N2}
exists {M3}
{AP:union M1 (map/+ N0 D2 M2) M3}
{E:eq M (map/+ N1 D1 M3)}
true.
- : union/<-inversion (union/< J P) P' _ J' eq/
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0P
<- map/+-preserves-eq N0=N0P unit`eq/ eq/ M022=M022'
<- union-respects-eq J eq/ M022=M022' eq/ J'.
- : union/<-inversion (union/= J' _ nat`eq/) N0+1+N=N M3 J E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F M2=M022
<- union-respects-eq J' eq/ M2=M022 eq/ J
<- false-implies-eq F E.
- : union/<-inversion (union/> J' N3+1+N2=N1) N0+1+N1=N2 M3 J E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M311=M1
<- false-implies-eq F M2=M022
<- union-respects-eq J' M311=M1 M2=M022 eq/ J
<- false-implies-eq F E.
%worlds () (union/<-inversion _ _ _ _ _).
%total {} (union/<-inversion _ _ _ _ _).
%reduces JP < J (union/<-inversion J _ _ JP _).
%theorem union/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3} {M}
forall {A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M}
{P:plus (s N3) N2 N1}
exists {M3}
{AP:union (map/+ N3 D1 M1) M2 M3}
{E:eq M (map/+ N2 D2 M3)}
true.
- : union/>-inversion (union/> J P) P' _ J' eq/
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N3+1=N3'+1
<- succ-cancels N3+1=N3'+1 N3=N3P
<- map/+-preserves-eq N3=N3P unit`eq/ eq/ M311=M311'
<- union-respects-eq J M311=M311' eq/ eq/ J'.
- : union/>-inversion (union/= J' _ nat`eq/) N3+1+N=N M3 J E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F M1=M311
<- union-respects-eq J' M1=M311 eq/ eq/ J
<- false-implies-eq F E.
- : union/>-inversion (union/< J' N0+1+N1=N2) N3+1+N2=N1 M3 J E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M1=M311
<- false-implies-eq F M022=M2
<- union-respects-eq J' M1=M311 M022=M2 eq/ J
<- false-implies-eq F E.
%worlds () (union/>-inversion _ _ _ _ _).
%total {} (union/>-inversion _ _ _ _ _).
%reduces JP < J (union/>-inversion J _ _ JP _).
%theorem union-deterministic :
forall* {M1} {M2} {M3} {M1P} {M2P} {M3P}
forall {A:union M1 M2 M3} {AP:union M1P M2P M3P}
{E1:eq M1 M1P} {E2:eq M2 M2P}
exists {E3:eq M3 M3P}
true.
- : union-deterministic union/L union/L eq/ eq/ eq/.
- : union-deterministic union/L union/R eq/ eq/ eq/.
- : union-deterministic union/R union/L eq/ eq/ eq/.
- : union-deterministic union/R union/R eq/ eq/ eq/.
- : union-deterministic (union/= M1+M2=M3 D1+D2=D3 nat`eq/)
(union/= M1+M2=M3' D1+D2=D3P nat`eq/)
eq/ eq/ M=M'
<- unit`union-deterministic D1+D2=D3 D1+D2=D3P unit`eq/ unit`eq/ D3=D3'
<- union-deterministic M1+M2=M3 M1+M2=M3' eq/ eq/ M3=M3'
<- map/+-preserves-eq nat`eq/ D3=D3' M3=M3' M=M'.
- : union-deterministic (union/< M1+MT=M3 N0+1+N1=N2)
(union/< M1+MT'=M3' N0'+1+N1=N2)
eq/ eq/ M=M'
<- plus-right-cancels N0+1+N1=N2 N0'+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0P
<- map/+-preserves-eq N0=N0P unit`eq/ eq/ MT=MT'
<- union-deterministic M1+MT=M3 M1+MT'=M3' eq/ MT=MT' M3=M3'
<- map/+-preserves-eq nat`eq/ unit`eq/ M3=M3' M=M'.
- : union-deterministic (union/> MT+M2=M3 N3+1+N2=N1)
(union/> MT'+M2=M3' N3'+1+N2=N1) eq/ eq/ E
<- plus-right-cancels N3+1+N2=N1 N3'+1+N2=N1 nat`eq/ nat`eq/ N3+1=N3'+1
<- succ-cancels N3+1=N3'+1 N3=N3P
<- map/+-preserves-eq N3=N3P unit`eq/ eq/ MT=MT'
<- union-deterministic MT+M2=M3 MT'+M2=M3' MT=MT' eq/ M3=M3'
<- map/+-preserves-eq nat`eq/ unit`eq/ M3=M3' E.
%% contradiction cases:
- : union-deterministic (union/= _ _ nat`eq/) (union/< _ N'+1+N=N) eq/ eq/ E
<- plus-implies-gt N'+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/= _ _ nat`eq/) (union/> _ N'+1+N=N) eq/ eq/ E
<- plus-implies-gt N'+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/< _ NP+1+N=N) (union/= _ _ nat`eq/) eq/ eq/ E
<- plus-implies-gt NP+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/< _ N0+1+N1=N2) (union/> _ N3+1+N2=N1) eq/ eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
- : union-deterministic (union/> _ NP+1+N=N) (union/= _ _ nat`eq/) eq/ eq/ E
<- plus-implies-gt NP+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/> _ N3+1+N2=N1) (union/< _ N0+1+N1=N2) eq/ eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (union-deterministic _ _ _ _ _).
%total (A) (union-deterministic A _ _ _ _).
%theorem union-total* :
forall {M1} {M2}
exists {M3} {A:union M1 M2 M3}
true.
%% we need some lemmas
%% We need them to ensure termination because
%% union substitutes new maps on recursive calls which
%% makes it hard to prove the arguments get smaller.
%theorem union-map/+-M-total* :
forall {N1} {D1} {M1} {M2}
exists {M3} {A:union (map/+ N1 D1 M1) M2 M3}
true.
%theorem union-M-map/+-total* :
forall {M1} {N2} {D2} {M2}
exists {M3} {A:union M1 (map/+ N2 D2 M2) M3}
true.
%theorem union-map/+-map/+-total* :
forall {N1} {D1} {M1} {N2} {D2} {M2} {C} {CMP:nat`compare N1 N2 C}
exists {M3}
{A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M3}
true.
- : union-total* map/0 M M union/L.
- : union-total* M map/0 M union/R.
- : union-total* (map/+ N1 D1 M1) (map/+ N2 D2 M2) M3 A
<- nat`compare-total* N1 N2 C CMP
<- union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 C CMP M3 A.
- : union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 equal CMP (map/+ N1 D3 M3)
(union/= M1+M2=M3 D1+D2=D3 N1=N2)
<- equal-implies-eq CMP N1=N2
<- unit`union-total* D1 D2 D3 D1+D2=D3
<- union-total* M1 M2 M3 M1+M2=M3.
- : union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 less CMP (map/+ N1 D1 M3)
(union/< M1+T=M3 N0+1+N1=N2)
<- less-implies-lt CMP N2>N1
<- gt-implies-plus N2>N1 _ N0+1+N1=N2
<- union-M-map/+-total* M1 N0 D2 M2 M3 M1+T=M3.
- : union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 greater CMP (map/+ N2 D2 M3)
(union/> T+M2=M3 N3+1+N2=N1)
<- greater-implies-gt CMP N1>N2
<- gt-implies-plus N1>N2 _ N3+1+N2=N1
<- union-map/+-M-total* N3 D1 M1 M2 M3 T+M2=M3.
- : union-M-map/+-total* map/0 N2 D2 M2 (map/+ N2 D2 M2) union/L.
- : union-M-map/+-total* (map/+ N1 D1 M1) N2 D2 M2 M3 A
<- nat`compare-total* N1 N2 C CMP
<- union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 C CMP M3 A.
- : union-map/+-M-total* N1 D1 M1 map/0 (map/+ N1 D1 M1) union/R.
- : union-map/+-M-total* N1 D1 M1 (map/+ N2 D2 M2) M3 A
<- nat`compare-total* N1 N2 C CMP
<- union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 C CMP M3 A.
%worlds () (union-total* _ _ _ _)
(union-M-map/+-total* _ _ _ _ _ _)
(union-map/+-M-total* _ _ _ _ _ _)
(union-map/+-map/+-total* _ _ _ _ _ _ _ _ _ _).
%total [ (M1a M1b M1c M1d) (M2a M2b M2c M2d) ]
(union-total* M1d M2d _ _)
(union-M-map/+-total* M1c _ _ M2c _ _)
(union-map/+-M-total* _ _ M1b M2b _ _)
(union-map/+-map/+-total* _ _ M1a _ _ M2a _ _ _ _).
%abbrev union-total = union-total* _ _ _.
%theorem disjoint-union-total :
forall* {M1} {M2}
forall {D:disjoint M1 M2}
exists {M3} {A:union M1 M2 M3}
true.
- : disjoint-union-total disjoint/L _ union/L.
- : disjoint-union-total disjoint/R _ union/R.
- : disjoint-union-total (disjoint/< D P) _ (union/< J P)
<- disjoint-union-total D _ J.
- : disjoint-union-total (disjoint/> D P) _ (union/> J P)
<- disjoint-union-total D _ J.
%worlds () (disjoint-union-total _ _ _).
%total (D) (disjoint-union-total D _ _).
%theorem union-empty-implies-empty :
forall* {M1} {M2}
forall {A:union M1 M2 map/0}
exists {E1:eq M1 map/0} {E2:eq M2 map/0}
true.
- : union-empty-implies-empty union/L eq/ eq/.
- : union-empty-implies-empty union/R eq/ eq/.
%worlds () (union-empty-implies-empty _ _ _).
%total { } (union-empty-implies-empty _ _ _).
%theorem union-preserves-disjoint* :
forall* {M1} {M2} {M3} {M4}
forall {D1:disjoint M1 M4} {D2:disjoint M2 M4}
{A:union M1 M2 M3}
exists {D3:disjoint M3 M4}
true.
% a lemma that counts the size of maps to help prove termination
%theorem union-preserves-disjoint*/L :
forall* {M1} {M2} {M3} {M4}
forall {S1} {S2} {SZ1:size M1 S1} {SZ2:size M2 S2}
{D1:disjoint M1 M4} {D2:disjoint M2 M4}
{A:union M1 M2 M3}
exists {D3:disjoint M3 M4}
true.
- : union-preserves-disjoint* D1 D2 J D3
<- size-total SZ1
<- size-total SZ2
<- union-preserves-disjoint*/L _ _ SZ1 SZ2 D1 D2 J D3.
- : union-preserves-disjoint*/L _ _ _ _ disjoint/R _ _ disjoint/R.
- : union-preserves-disjoint*/L _ _ _ _ _ disjoint/R _ disjoint/R.
- : union-preserves-disjoint*/L _ _ _ _ _ D union/L D.
- : union-preserves-disjoint*/L _ _ _ _ D _ union/R D.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/< D1 N5+1+N1=N4) D2X
(union/= J _ nat`eq/)
(disjoint/< D3 N5+1+N1=N4)
<- disjoint/<-inversion D2X N5+1+N1=N4 D2
<- union-preserves-disjoint*/L S1 S2 SZ1 SZ2 D1 D2 J D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/< D1 N5+1+N1=N4) D2X
(union/> J N3+1+N2=N1)
(disjoint/< D3 N6+1+N2=N4)
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 N5+1+N1=N4 N6 N5+1+N3=N6 N6+N2+1=N4
<- plus-swap-succ-converse N6+N2+1=N4 N6+1+N2=N4
<- disjoint/<-inversion D2X N6+1+N2=N4 D2
<- plus-swap-succ N5+1+N3=N6 N5+N3+1=N6
<- plus-commutative N5+N3+1=N6 N3+1+N5=N6
<- shift-right-preserves-disjoint D1 (shift/+ N3+1+N5=N6) D1< D1 N5+1+N4=N1) D2X
(union/= J DJ nat`eq/)
(disjoint/> D3 N5+1+N4=N1)
<- disjoint/>-inversion D2X N5+1+N4=N1 D2
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) (size/+ SZ2)
D1 D2 (union/= J DJ nat`eq/) D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/> D1 N5+1+N4=N1) D2X
(union/< J N0+1+N1=N2)
(disjoint/> D3 N5+1+N4=N1)
<- plus-swap-succ N5+1+N4=N1 N5+N4+1=N1
<- plus-associative-converse N5+N4+1=N1 N0+1+N1=N2 N6 N0+1+N5=N6 N6+N4+1=N2
<- plus-swap-succ-converse N6+N4+1=N2 N6+1+N4=N2
<- disjoint/>-inversion D2X N6+1+N4=N2 D2
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) (size/+ SZ2)
D1 D2 (union/< J N0+1+N5=N6) D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
D1X (disjoint/< D2 N6+1+N2=N4)
(union/< J N0+1+N1=N2)
(disjoint/< D3 N5+1+N1=N4)
<- plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- plus-associative-converse N0+N1+1=N2 N6+1+N2=N4 N5 N6+1+N0=N5 N5+N1+1=N4
<- plus-swap-succ-converse N5+N1+1=N4 N5+1+N1=N4
<- disjoint/<-inversion D1X N5+1+N1=N4 D1
<- plus-swap-succ N6+1+N0=N5 N6+N0+1=N5
<- plus-commutative N6+N0+1=N5 N0+1+N6=N5
<- shift-right-preserves-disjoint D2 (shift/+ N0+1+N6=N5) D2< D2 N6+1+N4=N2)
(union/> J N3+1+N2=N1)
(disjoint/> D3 N6+1+N4=N2)
<- plus-swap-succ N6+1+N4=N2 N6+N4+1=N2
<- plus-associative-converse N6+N4+1=N2 N3+1+N2=N1 N5 N3+1+N6=N5 N5+N4+1=N1
<- plus-swap-succ-converse N5+N4+1=N1 N5+1+N4=N1
<- disjoint/>-inversion D1X N5+1+N4=N1 D1
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) (size/+ SZ2)
D1 D2 (union/> J N3+1+N6=N5) D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/< D1 N5+1+N1=N4)
(disjoint/> D2 N6+1+N4=N2) JX D3X
<- plus-swap-succ N5+1+N1=N4 N5+N1+1=N4
<- plus-associative-converse N5+N1+1=N4 N6+1+N4=N2 N0 N6+1+N5=N0 N0+N1+1=N2
<- plus-swap-succ-converse N0+N1+1=N2 N0+1+N1=N2
<- union/<-inversion JX N0+1+N1=N2 _ J M=M113
<- eq-symmetric M=M113 M113=M
<- union-preserves-disjoint*/L S1 (s S2) SZ1 (size/+ SZ2)
D1 (disjoint/> D2 N6+1+N5=N0) J D3
<- disjoint-respects-eq (disjoint/< D3 N5+1+N1=N4) M113=M eq/ D3X.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/> D1 N5+1+N4=N1)
(disjoint/< D2 N6+1+N2=N4) JX D3X
<- plus-swap-succ N6+1+N2=N4 N6+N2+1=N4
<- plus-associative-converse N6+N2+1=N4 N5+1+N4=N1 N3 N5+1+N6=N3 N3+N2+1=N1
<- plus-swap-succ-converse N3+N2+1=N1 N3+1+N2=N1
<- union/>-inversion JX N3+1+N2=N1 _ J M=M223
<- eq-symmetric M=M223 M223=M
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) SZ2
(disjoint/> D1 N5+1+N6=N3) D2 J D3
<- disjoint-respects-eq (disjoint/< D3 N6+1+N2=N4) M223=M eq/ D3X.
%worlds () (union-preserves-disjoint*/L _ _ _ _ _ _ _ _).
%total {S1 S2 D1} (union-preserves-disjoint*/L S1 S2 _ _ D1 _ _ _).
%worlds () (union-preserves-disjoint* _ _ _ _).
%total { } (union-preserves-disjoint* _ _ _ _).
%theorem shift-left-preserves-union :
forall* {N} {D} {M1} {M2} {M3} {SM1}
forall {A:union M1 M2 M3} {S1:shift N M1 SM1}
exists {SA:union SM1 (map/+ N D M2) (map/+ N D M3)}
true.
- : shift-left-preserves-union union/L shift/0 union/L.
- : shift-left-preserves-union union/R shift/0 union/L.
- : shift-left-preserves-union M111+M2=M3 (shift/+ N+1+N1=N1')
(union/> M111+M2=M3 N1+1+N=N1')
<- plus-swap-succ N+1+N1=N1' N+N1+1=N1'
<- plus-commutative N+N1+1=N1' N1+1+N=N1'.
%worlds () (shift-left-preserves-union _ _ _).
%total { } (shift-left-preserves-union _ _ _).
%theorem shift-left-preserves-union-converse :
forall* {N} {D} {M1} {M2} {SM1} {SM3}
forall {SA:union SM1 (map/+ N D M2) SM3} {S1:shift N M1 SM1}
exists {M3} {A:union M1 M2 M3} {E:eq (map/+ N D M3) SM3}
true.
- : shift-left-preserves-union-converse union/L shift/0 _ union/L eq/.
- : shift-left-preserves-union-converse M111+M222=SM3 (shift/+ N2+1+N3=N1) M3
M311+M2=M3 M223=SM3
<- plus-swap-succ N2+1+N3=N1 N2+N3+1=N1
<- plus-commutative N2+N3+1=N1 N3+1+N2=N1
<- union/>-inversion M111+M222=SM3 N3+1+N2=N1 M3 M311+M2=M3 SM3=M223
<- eq-symmetric SM3=M223 M223=SM3.
%worlds () (shift-left-preserves-union-converse _ _ _ _ _).
%total { } (shift-left-preserves-union-converse _ _ _ _ _).
%theorem shift-right-preserves-union :
forall* {N} {D} {M1} {M2} {M3} {SM2}
forall {A:union M1 M2 M3} {S2:shift N M2 SM2}
exists {SA:union (map/+ N D M1) SM2 (map/+ N D M3)}
true.
- : shift-right-preserves-union union/L shift/0 union/R.
- : shift-right-preserves-union union/R shift/0 union/R.
- : shift-right-preserves-union M1+M222=M3 (shift/+ N+1+N2=N2')
(union/< M1+M222=M3 N2+1+N=N2')
<- plus-swap-succ N+1+N2=N2' N+N2+1=N2'
<- plus-commutative N+N2+1=N2' N2+1+N=N2'.
%worlds () (shift-right-preserves-union _ _ _).
%total { } (shift-right-preserves-union _ _ _).
%theorem shift-right-preserves-union-converse :
forall* {N} {D} {M1} {M2} {SM2} {SM3}
forall {SA:union (map/+ N D M1) SM2 SM3} {S2:shift N M2 SM2}
exists {M3} {A:union M1 M2 M3} {E:eq (map/+ N D M3) SM3}
true.
- : shift-right-preserves-union-converse union/R shift/0 _ union/R eq/.
- : shift-right-preserves-union-converse M111+M322=SM3 (shift/+ N1+1+N2=N3)
M3 M1+M222=M3 M133=SM3
<- plus-swap-succ N1+1+N2=N3 N1+N2+1=N3
<- plus-commutative N1+N2+1=N3 N2+1+N1=N3
<- union/<-inversion M111+M322=SM3 N2+1+N1=N3 M3 M1+M222=M3 SM3=M133
<- eq-symmetric SM3=M133 M133=SM3.
%worlds () (shift-right-preserves-union-converse _ _ _ _ _).
%total { } (shift-right-preserves-union-converse _ _ _ _ _).
%theorem shift-preserves-union :
forall* {N} {M1} {M2} {M3} {SM1} {SM2} {SM3}
forall {A:union M1 M2 M3}
{S1:shift N M1 SM1} {S2:shift N M2 SM2} {S3:shift N M3 SM3}
exists {SA:union SM1 SM2 SM3}
true.
- : shift-preserves-union union/L shift/0 M2< M311+M2=M3 N3+1+N2=N1)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(shift/+ N+1+N2=N6) M411+M522=M623
<- plus-deterministic N+1+N2=N5 N+1+N2=N6 nat`eq/ nat`eq/ N5=N6
<- plus-swap-succ N+1+N2=N5 N+N2+1=N5
<- plus-commutative N+N2+1=N5 N2+1+N=N5
<- plus-commutative N3+1+N2=N1 N2+N3+1=N1
<- plus-associative-converse* N2+N3+1=N1 N+1+N1=N4 N+1+N2=N5 N5+N3+1=N4
<- plus-commutative N5+N3+1=N4 N3+1+N5=N4
<- map/+-preserves-eq N5=N6 unit`eq/ eq/ M523=M623
<- union-respects-eq (union/> M311+M2=M3 N3+1+N5=N4) eq/ eq/ M523=M623
M411+M522=M623.
%worlds () (shift-preserves-union _ _ _ _ _).
%total { } (shift-preserves-union _ _ _ _ _).
%theorem shift-preserves-union-converse :
forall* {N} {M1} {M2} {SM1} {SM2} {SM3}
forall {SA:union SM1 SM2 SM3}
{S1:shift N M1 SM1} {S2:shift N M2 SM2}
exists {M3} {A:union M1 M2 M3} {S3:shift N M3 SM3}
true.
- : shift-preserves-union-converse union/L shift/0 M2< M611+M2=M3 N6+1+N5=N4)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5) _
(union/> M611+M2=M3 N6+1+N2=N1)
(shift/+ N+1+N2=N5)
<- plus-commutative N+1+N2=N5 N2+N+1=N5
<- plus-swap-succ-converse N2+N+1=N5 N2+1+N=N5
<- plus-associative-converse N2+N+1=N5 N6+1+N5=N4 N1' N6+1+N2=N1' N1'+N+1=N4
<- plus-commutative N+1+N1=N4 N1+N+1=N4
<- plus-right-cancels N1'+N+1=N4 N1+N+1=N4 nat`eq/ nat`eq/ N1'=N1
<- plus-respects-eq N6+1+N2=N1' nat`eq/ nat`eq/ N1'=N1 N6+1+N2=N1.
%worlds () (shift-preserves-union-converse _ _ _ _ _ _).
%total { } (shift-preserves-union-converse _ _ _ _ _ _).
%theorem union-commutative :
forall* {M1} {M2} {M3}
forall