Skip to content

Commit

Permalink
Improved lameq_BT_cong
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Feb 3, 2025
1 parent 39d4152 commit b44eef1
Show file tree
Hide file tree
Showing 6 changed files with 190 additions and 61 deletions.
18 changes: 17 additions & 1 deletion examples/generic_graphs/fsgraphScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
open HolKernel Parse boolLib bossLib;

open arithmeticTheory pairTheory listTheory pred_setTheory sortingTheory
hurdUtils topologyTheory;
hurdUtils topologyTheory relationTheory set_relationTheory;

open genericGraphTheory;

Expand Down Expand Up @@ -1044,6 +1044,22 @@ Proof
cheat
QED

Type vertex = “:unit + num”
Type edge = “:vertex set”

(* based on relationTheory
Definition preference_def :
preference (G :fsgraph) (R :vertex -> edge -> edge -> bool) <=>
!v. v IN nodes G ==> LinearOrder (R v)
End
*)

(* based on set_relationTheory *)
Definition preference_def :
preference (G :fsgraph) (R :vertex -> edge # edge -> bool) <=>
!v. v IN nodes G ==> linear_order (R v) (fsgedges G)
End

(* ----------------------------------------------------------------------
Menger's Theorem [2, p.67], added by Chun Tian
----------------------------------------------------------------------
Expand Down
50 changes: 19 additions & 31 deletions examples/lambda/barendregt/boehmScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1723,7 +1723,7 @@ Proof
qabbrev_tac ‘x' = lswapstr (REVERSE p1) x’ \\
‘x' IN FV M2’ by METIS_TAC [SUBSET_DEF] \\
Know ‘FV M2 SUBSET FV (M0 @* MAP VAR vs2)’
>- (‘solvable M2’ by rw [solvable_iff_has_hnf, hnf_has_hnf] \\
>- (‘solvable M2’ by rw [hnf_solvable] \\
‘M0 @* MAP VAR vs2 == M2’ by rw [] \\
qunabbrev_tac ‘M2’ \\
MATCH_MP_TAC principle_hnf_FV_SUBSET' \\
Expand Down Expand Up @@ -1776,7 +1776,7 @@ Proof
DISCH_TAC (* x' IN FV N *) \\
‘x' IN FV M2’ by METIS_TAC [SUBSET_DEF] \\
Know ‘FV M2 SUBSET FV (M0 @* MAP VAR vs2)’
>- (‘solvable M2’ by rw [solvable_iff_has_hnf, hnf_has_hnf] \\
>- (‘solvable M2’ by rw [hnf_solvable] \\
‘M0 @* MAP VAR vs2 == M2’ by rw [] \\
qunabbrev_tac ‘M2’ \\
MATCH_MP_TAC principle_hnf_FV_SUBSET' \\
Expand Down Expand Up @@ -2217,8 +2217,7 @@ Proof
‘LAMl vs (VAR y @* args) @* MAP VAR vs == VAR y @* args’
by PROVE_TAC [lameq_LAMl_appstar_VAR] \\
Suff ‘solvable (VAR y @* args)’ >- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> simp [hnf_appstar])
MATCH_MP_TAC hnf_solvable >> simp [hnf_appstar])
>> Rewr'
>> simp [principle_hnf_beta_reduce, hnf_appstar, tpm_appstar]
>> rw [Abbr ‘f’]
Expand Down Expand Up @@ -2294,8 +2293,7 @@ Proof
‘LAMl vs (VAR y @* args) @* MAP VAR vs == VAR y @* args’
by PROVE_TAC [lameq_LAMl_appstar_VAR] \\
Suff ‘solvable (VAR y @* args)’ >- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf \\
MATCH_MP_TAC hnf_solvable \\
simp [hnf_appstar])
>> Rewr'
>> simp [principle_hnf_beta_reduce, hnf_appstar, tpm_appstar]
Expand Down Expand Up @@ -2907,8 +2905,8 @@ Proof
>- (Suff ‘solvable ([P/v] M0)’ >- PROVE_TAC [lameq_solvable_cong] \\
simp [LAMl_SUB, appstar_SUB] \\
reverse (Cases_on ‘y = v’)
>- (simp [SUB_THM, solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) \\
>- (simp [SUB_THM] \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar]) \\
simp [solvable_iff_has_hnf, has_hnf_thm] \\
qabbrev_tac ‘args' = MAP [P/v] args’ \\
qabbrev_tac ‘m = LENGTH args’ \\
Expand Down Expand Up @@ -5122,8 +5120,8 @@ Proof
>> Know ‘solvable (apply pi M)’
>- (Suff ‘solvable (VAR b @* args' @* MAP VAR as)’
>- METIS_TAC [lameq_solvable_cong] \\
simp [solvable_iff_has_hnf, GSYM appstar_APPEND] \\
MATCH_MP_TAC hnf_has_hnf >> simp [hnf_appstar])
MATCH_MP_TAC hnf_solvable \\
simp [GSYM appstar_APPEND, hnf_appstar])
>> DISCH_TAC
(* stage work *)
>> Know ‘principle_hnf (apply pi M) = VAR b @* args' @* MAP VAR as’
Expand Down Expand Up @@ -5182,14 +5180,12 @@ Proof
by rw [lameq_appstar_cong] \\
Suff ‘solvable (M1 @* MAP VAR (SNOC b as))’
>- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar]) \\
CONJ_TAC (* has_hnf #2 *)
>- (REWRITE_TAC [GSYM solvable_iff_has_hnf] \\
Suff ‘solvable (VAR b @* args' @* MAP VAR as)’
>- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar]) \\
CONJ_TAC (* has_hnf # 3 *)
>- (simp [appstar_SUB, MAP_SNOC] \\
Know ‘MAP [P/y] (MAP VAR as) = MAP VAR as’
Expand All @@ -5207,8 +5203,7 @@ Proof
>- (MATCH_MP_TAC permutator_thm >> rw []) >> DISCH_TAC \\
Suff ‘solvable (VAR b @* (args' ++ MAP VAR as))’
>- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar]) \\
(* applying the celebrating principle_hnf_denude_thm
NOTE: here ‘DISJOINT (set vs) (FV M)’ is required, and this means that
Expand Down Expand Up @@ -6058,8 +6053,7 @@ Proof
‘M0 i @* MAP VAR vs = apply p1 (M0 i)’
by rw [Abbr ‘p1’, Boehm_apply_MAP_rightctxt'] >> POP_ORW \\
Suff ‘solvable (M1 i)’ >- METIS_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf \\
MATCH_MP_TAC hnf_solvable \\
rw [GSYM appstar_APPEND, hnf_appstar]) \\
REWRITE_TAC [FV_appstar_MAP_VAR] \\
Know ‘y i IN FV (M1 i) /\
Expand Down Expand Up @@ -6123,9 +6117,7 @@ Proof
MP_TAC (Q.SPEC ‘M0 (i :num) @* MAP VAR vs'’ principle_hnf_FV_SUBSET') \\
impl_tac >- (Suff ‘solvable (VAR (y i) @* args i)’
>- METIS_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf \\
simp [hnf_appstar]) \\
MATCH_MP_TAC hnf_solvable >> simp [hnf_appstar]) \\
POP_ORW \\
REWRITE_TAC [FV_appstar_MAP_VAR, FV_appstar, FV_thm] \\
SET_TAC [])
Expand Down Expand Up @@ -6313,8 +6305,7 @@ Proof
P (f i) @* Ns i @@ VAR (b i) @* tl i == VAR (b i) @* Ns i @* tl i’
>- (METIS_TAC [lameq_solvable_cong]) \\
reverse CONJ_TAC >- (MATCH_MP_TAC hreduces_lameq >> rw []) \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> art []) >> Rewr' \\
MATCH_MP_TAC hnf_solvable >> art []) >> Rewr' \\
Know ‘P (f i) @* args' i @* args2 i @* MAP VAR xs = M1 i @* MAP VAR xs ISUB ss’
>- (REWRITE_TAC [appstar_ISUB, Once EQ_SYM_EQ] \\
Q.PAT_X_ASSUM ‘!i. i < k ==> apply p2 (M1 i) = _’
Expand All @@ -6338,14 +6329,12 @@ Proof
‘M0' == M1 i’ by rw [Abbr ‘M0'’] \\
‘M0' @* MAP VAR xs == M1 i @* MAP VAR xs’ by rw [lameq_appstar_cong] \\
Suff ‘solvable (M1 i @* MAP VAR xs)’ >- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar]) \\
CONJ_TAC (* has_hnf #2 *)
>- (REWRITE_TAC [GSYM solvable_iff_has_hnf] \\
Suff ‘solvable (VAR (b i) @* Ns i @* tl i)’
>- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar]) \\
CONJ_TAC (* has_hnf # 3 *)
>- (simp [appstar_ISUB, MAP_DROP] \\
ASM_SIMP_TAC bool_ss [has_hnf_thm] \\
Expand Down Expand Up @@ -6383,8 +6372,7 @@ Proof
>- (rpt STRIP_TAC \\
Suff ‘solvable (VAR (b i) @* Ns i @* tl i)’
>- METIS_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar, GSYM appstar_APPEND])
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar, GSYM appstar_APPEND])
>> DISCH_TAC
>> PRINT_TAC "stage work on subtree_equiv_lemma: L6433"
>> CONJ_TAC (* EVERY is_ready ... *)
Expand Down Expand Up @@ -6803,8 +6791,8 @@ Proof
(* ‘H i’ is the head reduction of apply pi (M i) *)
>> qabbrev_tac ‘H = \i. VAR (b i) @* Ns i @* tl i’
>> Know ‘!i. solvable (H i)’
>- (rw [Abbr ‘H’, solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar])
>- (rw [Abbr ‘H’] \\
MATCH_MP_TAC hnf_solvable >> rw [hnf_appstar])
>> DISCH_TAC
>> Know ‘!i. i < k ==> FV (H i) SUBSET X UNION RANK r’
>- (simp [Abbr ‘H’, GSYM appstar_APPEND, FV_appstar] \\
Expand Down
27 changes: 20 additions & 7 deletions examples/lambda/barendregt/chap3Script.sml
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,21 @@
open HolKernel Parse boolLib bossLib;
(* ========================================================================== *)
(* FILE : chap3Script.sml *)
(* TITLE : Theory of reductions (Chapter 3 of Barendregt 1984 [1]) *)
(* *)
(* AUTHORS : 2005-2011 Michael Norrish *)
(* : 2023-2025 Michael Norrish and Chun Tian *)
(* ========================================================================== *)

open boolSimps metisLib basic_swapTheory relationTheory listTheory hurdUtils;
open HolKernel Parse boolLib bossLib;

local open pred_setLib in end;
open boolSimps metisLib basic_swapTheory relationTheory listTheory hurdUtils
pred_setTheory pred_setLib BasicProvers;

open binderLib BasicProvers nomsetTheory termTheory chap2Theory appFOLDLTheory;
open horeductionTheory
open binderLib nomsetTheory termTheory chap2Theory appFOLDLTheory
horeductionTheory;

val _ = new_theory "chap3";

val SUBSET_DEF = pred_setTheory.SUBSET_DEF

(* definition from p30 *)
val beta_def = Define`beta M N = ?x body arg. (M = LAM x body @@ arg) /\
(N = [arg/x]body)`;
Expand Down Expand Up @@ -125,6 +130,14 @@ val cc_beta_FV_SUBSET = store_thm(
HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN
SRW_TAC [][SUBSET_DEF, FV_SUB] THEN PROVE_TAC []);

Theorem betastar_FV_SUBSET :
!M N. M -b->* N ==> FV N SUBSET FV M
Proof
HO_MATCH_MP_TAC RTC_INDUCT >> rw []
>> Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV M'’ >> art []
>> MATCH_MP_TAC cc_beta_FV_SUBSET >> art []
QED

Theorem cc_beta_tpm:
!M N. M -b-> N ==> !p. tpm p M -b-> tpm p N
Proof
Expand Down
Loading

0 comments on commit b44eef1

Please sign in to comment.