Skip to content

Commit

Permalink
Stage work on ltree_insert_delete'
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Feb 27, 2025
1 parent 65461bd commit 9ddece6
Show file tree
Hide file tree
Showing 2 changed files with 214 additions and 1 deletion.
37 changes: 37 additions & 0 deletions src/coalgebras/llistScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2202,6 +2202,43 @@ Proof
>> qexistsl_tac [‘x’, ‘n’] >> rw []
QED

val LFINITE_strongind = DB.fetch "-" "LFINITE_strongind";

Theorem LNTH_IS_SOME_lemma[local] :
!ll. LFINITE ll ==> !n. n < THE (LLENGTH ll) ==> IS_SOME (LNTH n ll)
Proof
HO_MATCH_MP_TAC LFINITE_strongind
>> rw []
>> gs [LFINITE_LLENGTH]
>> Cases_on ‘n’ >> rw [LNTH_THM]
QED

Theorem LNTH_IS_SOME :
!n ll. IS_SOME (LNTH n ll) <=> (LFINITE ll ==> n < THE (LLENGTH ll))
Proof
rpt GEN_TAC
>> reverse EQ_TAC
>- (rpt STRIP_TAC \\
reverse (Cases_on ‘LFINITE ll’)
>- (fs [LFINITE_LNTH_NONE] \\
POP_ASSUM (MP_TAC o Q.SPEC ‘n’) \\
rw [IS_SOME_EQ_NOT_NONE]) \\
irule LNTH_IS_SOME_lemma >> simp [])
>> rw [LFINITE_LLENGTH] >> rw []
>> rename1 ‘i < N’
>> fs [IS_SOME_EXISTS]
>> CCONTR_TAC
>> ‘N <= i’ by rw []
>> ‘LNTH i ll = NONE’ by PROVE_TAC [LNTH_LLENGTH_NONE]
>> fs []
QED

Theorem LFINITE_LNTH_IS_SOME :
!n ll. LFINITE ll ==> (IS_SOME (LNTH n ll) <=> n < THE (LLENGTH ll))
Proof
rw [LNTH_IS_SOME]
QED

(* ------------------------------------------------------------------------ *)
(* Turning a stream-like linear order into a lazy list *)
(* ------------------------------------------------------------------------ *)
Expand Down
178 changes: 177 additions & 1 deletion src/coalgebras/ltreeScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1051,12 +1051,188 @@ Proof
>> rw [ltree_paths_def]
QED

Theorem ltree_branching_thm :
!h p a ts. h::p IN ltree_paths (Branch a ts) ==>
ltree_branching (Branch a ts) (h::p) =
ltree_branching (THE (LNTH h ts)) p
Proof
rpt GEN_TAC
>> rw [ltree_paths_alt_ltree_el, ltree_el_def, ltree_branching_def]
>> Cases_on ‘LNTH h ts’ >> fs []
QED

(* NOTE: The proof based on ltree_bisimulation is smaller *)
Theorem gen_ltree_unchanged :
!t. gen_ltree (\p. THE (ltree_el t p)) = t
Proof
Q.X_GEN_TAC ‘t’
>> rw [ltree_bisimulation]
>> Q.EXISTS_TAC ‘\x y. x = gen_ltree (\p. THE (ltree_el y p))’
>> simp []
>> rpt STRIP_TAC
>- fs [Once gen_ltree, ltree_el_def]
>> rw [llist_rel_def]
>- fs [Once gen_ltree, ltree_el_def]
>> fs [Once gen_ltree, ltree_el_def, LNTH_EQ, LNTH_LGENLIST]
>> Q.PAT_X_ASSUM ‘!n. P’ (MP_TAC o Q.SPEC ‘i’)
>> simp []
>> Cases_on ‘y’ >> simp [ltree_el_def]
>> Cases_on ‘LLENGTH ts'’ >> simp []
>- (DISCH_THEN (fs o wrap) \\
simp [Once gen_ltree, ltree_el_def])
>> rw []
>> simp [Once gen_ltree, ltree_el_def]
QED

(* NOTE: This is another (longer) proof (by ltree_el_eqv) *)
Theorem gen_ltree_unchanged_by_ltree_el_eqv[local] :
!t. gen_ltree (\p. THE (ltree_el t p)) = t
Proof
Q.X_GEN_TAC ‘t’
>> simp [ltree_el_eqv]
>> Q.X_GEN_TAC ‘q’
>> qid_spec_tac ‘t’
>> Induct_on ‘q’
>- (Cases_on ‘t’ >> simp [ltree_el_def] \\
simp [Once gen_ltree, ltree_el_def])
(* stage work *)
>> rpt GEN_TAC
>> Cases_on ‘t’ >> simp [ltree_el_def]
>> simp [Once gen_ltree, ltree_el_def, LNTH_LGENLIST]
>> Cases_on ‘LLENGTH ts’ >> simp []
>- (Cases_on ‘LNTH h ts’ >> simp [] \\
Know ‘~LFINITE ts’
>- gs [LFINITE_LLENGTH] \\
rw [infinite_lnth_some] \\
POP_ASSUM (MP_TAC o Q.SPEC ‘h’) >> rw [])
>> Cases_on ‘LNTH h ts’ >> simp []
>- (‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
Know ‘~(h < x)’
>- (‘x = THE (LLENGTH ts)’ by rw [] >> POP_ORW \\
rw [GSYM LFINITE_LNTH_IS_SOME]) \\
rw [])
>> rename1 ‘LNTH h ts = SOME t0’
>> ‘LFINITE ts’ by rw [LFINITE_LLENGTH]
>> Know ‘h < x’
>- (‘x = THE (LLENGTH ts)’ by rw [] >> POP_ORW \\
rw [GSYM LFINITE_LNTH_IS_SOME])
>> rw []
QED

(* NOTE: This proof is smart in handling f in the bisimulation construction *)
Theorem gen_ltree_unchanged_extra :
!t f. gen_ltree (\p. if ltree_el t p <> NONE then THE (ltree_el t p)
else f p) = t
Proof
rw [ltree_bisimulation]
>> Q.EXISTS_TAC ‘\x y. ?f. x = gen_ltree (\p. if ltree_el y p <> NONE then
THE (ltree_el y p)
else f p)’
>> CONJ_TAC
>- (simp [] >> Q.EXISTS_TAC ‘f’ >> simp [])
>> rpt STRIP_TAC
>- fs [Once gen_ltree, ltree_el_def]
>> rw [llist_rel_def]
>- fs [Once gen_ltree, ltree_el_def]
>> fs [Once gen_ltree, ltree_el_def, LNTH_EQ, LNTH_LGENLIST]
>> Q.PAT_X_ASSUM ‘!n. P’ (MP_TAC o Q.SPEC ‘i’)
>> simp []
>> Cases_on ‘y’ >> simp [ltree_el_def]
>> Cases_on ‘LLENGTH ts'’ >> simp []
>- (DISCH_THEN (fs o wrap) \\
simp [Once gen_ltree, ltree_el_def] \\
Q.EXISTS_TAC ‘\p. f (i::p)’ >> simp [])
>> rw []
>> simp [Once gen_ltree, ltree_el_def]
>> Q.EXISTS_TAC ‘\p. f (i::p)’ >> simp []
QED

Theorem ltree_insert_delete' :
!p t t0. ltree_lookup t (SNOC n p) = SOME t0 /\
ltree_branching t p = SOME (SUC n) ==>
ltree_insert' (ltree_delete' t p) p t0 = t
Proof
cheat
(* initial preparation *)
rpt STRIP_TAC
>> Know ‘p IN ltree_paths t’
>- (MATCH_MP_TAC ltree_paths_inclusive \\
Q.EXISTS_TAC ‘SNOC n p’ \\
rw [isPREFIX_SNOC, ltree_paths_def])
>> DISCH_TAC
>> Q.PAT_X_ASSUM ‘ltree_lookup t (SNOC n p) = SOME t0’ MP_TAC
>> Know ‘ltree_lookup t (SNOC n p) =
ltree_lookup (THE (ltree_lookup t p)) [n]’
>- (MATCH_MP_TAC ltree_lookup_SNOC \\
fs [ltree_paths_def])
>> Rewr'
>> POP_ASSUM MP_TAC
>> simp [ltree_paths_def]
>> simp [GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
>> STRIP_TAC
>> Cases_on ‘x’
>> simp [ltree_lookup_def]
>> Cases_on ‘LNTH n ts’ >> simp []
>> DISCH_THEN (fs o wrap)
>> fs [ltree_branching_def]
>> MP_TAC (Q.SPECL [‘p’, ‘t’] ltree_el_alt_ltree_lookup)
>> rw [ltree_paths_def]
>> POP_ASSUM (fs o wrap)
(* stage work *)
>> rpt (POP_ASSUM MP_TAC)
>> qid_spec_tac ‘t0’
>> qid_spec_tac ‘t’
>> qid_spec_tac ‘a’
>> qid_spec_tac ‘ts’
>> qid_spec_tac ‘n’
>> qid_spec_tac ‘p’
>> Induct_on ‘p’
>- (rw [ltree_lookup] \\
(* 1. eliminating ltree_delete *)
simp [ltree_delete_def] \\
simp [Once gen_ltree, ltree_el_def] \\
qmatch_abbrev_tac ‘ltree_insert' t' [] t0 = _’ \\
Know ‘t' = Branch a (LGENLIST (\i. THE (LNTH i ts)) (SOME n))’
>- (simp [Abbr ‘t'’] \\
simp [LNTH_EQ, LNTH_LGENLIST] \\
Q.X_GEN_TAC ‘i’ \\
Cases_on ‘i < n’ >> simp [] \\
Cases_on ‘LNTH i ts’ >> simp []
>- (Know ‘IS_SOME (LNTH i ts)’
>- (MATCH_MP_TAC LNTH_IS_SOME_MONO \\
Q.EXISTS_TAC ‘n’ >> simp [IS_SOME_EXISTS]) \\
rw [IS_SOME_EXISTS]) \\
Know ‘!p. (\(d,len). (d,len)) (THE (ltree_el x p)) = THE (ltree_el x p)’
>- (rpt GEN_TAC \\
qabbrev_tac ‘a = THE (ltree_el x p)’ \\
Cases_on ‘a’ >> simp []) >> Rewr' \\
simp [gen_ltree_unchanged]) >> Rewr' \\
qunabbrev_tac ‘t'’ \\
(* 2. eliminating ltree_insert *)
simp [ltree_insert_def] \\
simp [Once gen_ltree, ltree_el_def, LNTH_LGENLIST] \\
(* applying LNTH_EQ again *)
simp [LNTH_EQ, LNTH_LGENLIST, GSYM ADD1] \\
Q.X_GEN_TAC ‘i’ \\
‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
reverse (Cases_on ‘i < SUC n’ >> simp [])
>- (MATCH_MP_TAC (GEN_ALL LNTH_LLENGTH_NONE) \\
Q.EXISTS_TAC ‘SUC n’ >> rw []) \\
‘i = n \/ i < n’ by rw [] >> simp [] >- rw [gen_ltree_unchanged] \\
(* so far so good ... *)
qabbrev_tac ‘t1 = THE (LNTH i ts)’ \\
Know ‘!p. (\(d,len). (d,len)) (THE (ltree_el t1 p)) = THE (ltree_el t1 p)’
>- (rpt GEN_TAC \\
qabbrev_tac ‘a = THE (ltree_el t1 p)’ \\
Cases_on ‘a’ >> simp []) >> Rewr' \\
(* so far so good ... *)
‘IS_SOME (LNTH i ts)’ by rw [LFINITE_LNTH_IS_SOME] \\
fs [IS_SOME_EXISTS, Abbr ‘t1’] \\
rw [gen_ltree_unchanged_extra])
(* stage work *)
>> rpt GEN_TAC
>> Cases_on ‘t’ >> simp [ltree_lookup_def]
>> Cases_on ‘LNTH h ts'’ >> rw []
>> cheat
QED

(*---------------------------------------------------------------------------*
Expand Down

0 comments on commit 9ddece6

Please sign in to comment.