Skip to content

Add LIST_REL aliases for EVERY2 theorems #1772

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Open
xrchz wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Add LIST_REL aliases for EVERY2 theorems #1772

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 22 additions & 0 deletions src/list/src/listScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2363,6 +2363,8 @@ Proof
METIS_TAC[]
QED

Theorem LIST_REL_cong = EVERY2_cong

Theorem MAP_EQ_EVERY2:
!f1 f2 l1 l2. (MAP f1 l1 = MAP f2 l2) <=>
(LENGTH l1 = LENGTH l2) /\
Expand All @@ -2374,6 +2376,8 @@ Cases_on ‘l2’ THEN SRW_TAC [] [MAP] THEN
PROVE_TAC[]
QED

Theorem MAP_EQ_LIST_REL = MAP_EQ_EVERY2

Theorem EVERY2_EVERY:
!l1 l2 f. EVERY2 f l1 l2 <=>
LENGTH l1 = LENGTH l2 /\ EVERY (UNCURRY f) (ZIP (l1,l2))
Expand All @@ -2382,6 +2386,8 @@ Induct THEN1 SRW_TAC [] [LENGTH_NIL_SYM, EQ_IMP_THM, ZIP] THEN
GEN_TAC THEN Cases THEN SRW_TAC [] [ZIP, EQ_IMP_THM]
QED

Theorem LIST_REL_EVERY = EVERY2_EVERY

Theorem EVERY2_LENGTH:
!P l1 l2. EVERY2 P l1 l2 ==> (LENGTH l1 = LENGTH l2)
Proof
Expand Down Expand Up @@ -4646,6 +4652,8 @@ Proof
>> ASM_SIMP_TAC (arith_ss) []
QED

Theorem LIST_REL_REVERSE = EVERY2_REVERSE

Theorem SUM_MAP_PLUS:
!f g ls. SUM (MAP (\x. f x + g x) ls) = SUM (MAP f ls) + SUM (MAP g ls)
Proof
Expand Down Expand Up @@ -4693,6 +4701,8 @@ Proof
THEN METIS_TAC []
QED

Theorem LIST_REL_trans_same = EVERY2_trans

Theorem EVERY2_sym:
(!x y. R1 x y ==> R2 y x) ==> !x y. EVERY2 R1 x y ==> EVERY2 R2 y x
Proof
Expand All @@ -4702,6 +4712,8 @@ Proof
THEN FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP]
QED

Theorem LIST_REL_sym = EVERY2_sym

Theorem EVERY2_LUPDATE_same:
!P l1 l2 v1 v2 n.
P v1 v2 /\ EVERY2 P l1 l2 ==>
Expand All @@ -4716,12 +4728,16 @@ Proof
THEN FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]
QED

Theorem LIST_REL_LUPDATE_same = EVERY2_LUPDATE_same

Theorem EVERY2_refl:
(!x. MEM x ls ==> R x x) ==> (EVERY2 R ls ls)
Proof
Induct_on‘ls’ >> rw []
QED

Theorem LIST_REL_refl = EVERY2_refl

Theorem EVERY2_THM[simp]:
(!P ys. EVERY2 P [] ys = (ys = [])) /\
(!P yys x xs. EVERY2 P (x::xs) yys =
Expand All @@ -4739,6 +4755,8 @@ Proof
THEN SRW_TAC [] [EVERY2_EVERY]
QED

Theorem LIST_REL_THM = EVERY2_THM

Theorem LIST_REL_trans:
!l1 l2 l3.
(!n. n < LENGTH l1 /\ R (EL n l1) (EL n l2) /\
Expand Down Expand Up @@ -5012,6 +5030,8 @@ Proof
>> SRW_TAC [DNF_ss] [pairTheory.FORALL_PROD, LENGTH_MAP, MEM_ZIP]
QED

Theorem LIST_REL_MAP = EVERY2_MAP

Theorem exists_list_GENLIST:
(?ls. P ls) = (?n f. P (GENLIST f n))
Proof
Expand All @@ -5037,6 +5057,8 @@ Proof
rw [EVERY2_EVERY] >> MATCH_MP_TAC EVERY_MEM_MONO >> PROVE_TAC []
QED

Theorem LIST_REL_MEM_MONO = EVERY2_MEM_MONO

Theorem mem_exists_set:
!x y l. MEM (x,y) l ==> ?z. (x = FST z) /\ z IN set l
Proof
Expand Down
8 changes: 8 additions & 0 deletions src/list/src/rich_listScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4232,13 +4232,17 @@ Proof
Induct_on ‘n’ >> simp[] >> Induct_on ‘l1’ >> dsimp[]
QED

Theorem LIST_REL_DROP = EVERY2_DROP

Theorem EVERY2_TAKE:
!P xs ys n. EVERY2 P xs ys ==> EVERY2 P (TAKE n xs) (TAKE n ys)
Proof
Induct_on ‘n’ >> simp[] >> Induct_on ‘xs’ >>
asm_simp_tac (srw_ss() ++ boolSimps.DNF_ss) []
QED

Theorem LIST_REL_TAKE = EVERY2_TAKE

Theorem LIST_REL_APPEND_SING[simp]:
LIST_REL R (l1 ++ [x1]) (l2 ++ [x2]) <=> LIST_REL R l1 l2 /\ R x1 x2
Proof
Expand All @@ -4257,6 +4261,8 @@ Proof
>> fs [DECIDE ``i < SUC n <=> i < n \/ (i = n)``] >> METIS_TAC []
QED

Theorem EVERY2_GENLIST = LIST_REL_GENLIST

Theorem ALL_DISTINCT_MEM_ZIP_MAP:
!f x ls.
ALL_DISTINCT ls ==>
Expand Down Expand Up @@ -4293,6 +4299,8 @@ Proof
>> simp[REVERSE_ZIP, Excl "EVERY_REVERSE"]
QED

Theorem LIST_REL_REVERSE1 = EVERY2_REVERSE1

Theorem LIST_REL_REVERSE_EQ[simp]:
LIST_REL R (REVERSE l1) (REVERSE l2) <=> LIST_REL R l1 l2
Proof
Expand Down