Skip to content

Commit

Permalink
Add more primitive proof rules
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0 @mn200
digama0 authored and mn200 committed Sep 23, 2024
1 parent 04bef39 commit 72a01e7
Show file tree
Hide file tree
Showing 4 changed files with 131 additions and 44 deletions.
1 change: 1 addition & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
*.ui
*.o
.hollogs
.holobjs
.HOLMK
*.lex.sml
*.grm.sig
Expand Down
26 changes: 21 additions & 5 deletions src/opentheory/postbool/Logging.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ val _ = Feedback.register_trace("opentheory logging",verbosity,5)

val proof_type = let open Thm fun
f Axiom_prf = "Axiom"
|f deleted_prf = "deleted"
|f (ABS_prf _) = "ABS"
|f (ALPHA_prf _) = "ALPHA"
|f (AP_TERM_prf _) = "AP_TERM"
Expand All @@ -35,6 +36,7 @@ val proof_type = let open Thm fun
|f (EQ_MP_prf _) = "EQ_MP"
|f (EXISTS_prf _) = "EXISTS"
|f (GEN_prf _) = "GEN"
|f (GENL_prf _) = "GENL"
|f (GEN_ABS_prf _) = "GEN_ABS"
|f (INST_TYPE_prf _) = "INST_TYPE"
|f (INST_prf _) = "INST"
Expand All @@ -56,6 +58,7 @@ val proof_type = let open Thm fun
|f (Mk_comb_prf _) = "Mk_comb"
|f (Specialize_prf _) = "Specialize"
|f (deductAntisym_prf _) = "deductAntisym"
|f compute_prf = "compute"
in f end

datatype log_state =
Expand Down Expand Up @@ -282,7 +285,14 @@ val (log_term, log_thm, log_clear,
val GEN_pth = let
val th1 = ASSUME (mk_eq(P,mk_abs(x,T)))
val th2 = AP_THM FORALL_DEF P
in EQ_MP (SYM(CONV_RULE(RAND_CONV BETA_CONV) th2)) th1 end
val pth = EQ_MP (SYM(CONV_RULE(RAND_CONV BETA_CONV) th2)) th1
in
fn v => fn th => let
val vty = type_of v
val P = mk_var("P",vty-->bool)
val pth = INST_TY_TERM ([P|->mk_abs(v,concl th)],[alpha|->vty]) pth
in proveHyp (ABS v (eqtIntro th)) pth end
end
val Q = mk_var("Q",bool)
val EXISTS_pth = let
val th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P)
Expand Down Expand Up @@ -394,6 +404,11 @@ val (log_term, log_thm, log_clear,
val _ = log_term (concl th)
val _ = log_command "axiom"
in () end
| deleted_prf => let
val _ = log_list log_term (hyp th)
val _ = log_term (concl th)
val _ = log_command "axiom"
in () end
| ASSUME_prf tm => let
val _ = log_term tm
val _ = log_command "assume"
Expand Down Expand Up @@ -534,10 +549,10 @@ val (log_term, log_thm, log_clear,
val _ = log_thm (EQ_MP (rconv fvs source tm) sth)
in () end
| GEN_prf (v,th) => let
val vty = type_of v
val P = mk_var("P",vty-->bool)
val pth = INST_TY_TERM ([P|->mk_abs(v,concl th)],[alpha|->vty]) GEN_pth
val _ = log_thm (proveHyp (ABS v (eqtIntro th)) pth)
val _ = log_thm (GEN_pth v th)
in () end
| GENL_prf (vs,th) => let
val _ = log_thm (itlist GEN_pth vs th)
in () end
| DISJ1_prf (th,tm) => let
val _ = log_thm (proveHyp th (INST [P|->concl th,Q|->tm] DISJ1_pth))
Expand Down Expand Up @@ -671,6 +686,7 @@ val (log_term, log_thm, log_clear,
[alpha|->rty,beta|->aty]) Def_tyop_pth
val _ = log_thm (proveHyp ra (proveHyp ar pth))
in () end
| compute_prf => raise ERR "log_thm" "disabled in opentheory kernel";
val _ = if !verbosity >= 4 then HOL_MESG("Finish proof for "^(Susp.force ths)) else ()
(*
val _ = log_comment(pt^")")
Expand Down
145 changes: 106 additions & 39 deletions src/thm/otknl-thm.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ end;
datatype thm = THM of Tag.tag * term HOLset.set * term * proof ref
and proof =
Axiom_prf
| deleted_prf
| ASSUME_prf of term
| REFL_prf of term
| BETA_CONV_prf of term
Expand All @@ -131,6 +132,7 @@ and proof =
| EQ_IMP_RULE2_prf of thm
| SPEC_prf of term * thm
| GEN_prf of term * thm
| GENL_prf of term list * thm
| EXISTS_prf of term * term * thm
| CHOOSE_prf of term * thm * thm
| CONJ_prf of thm * thm
Expand All @@ -151,9 +153,10 @@ and proof =
| Def_const_list_prf of string * (string * hol_type) list * thm
| Def_spec_prf of term list * thm
| deductAntisym_prf of thm * thm
| compute_prf

fun proof (THM(_,_,_,p)) = !p
fun delete_proof (THM(_,_,_,p)) = p := Axiom_prf
fun delete_proof (THM(_,_,_,p)) = p := deleted_prf

fun single_hyp tm = HOLset.singleton Term.compare tm
val empty_hyp = Term.empty_tmset
Expand Down Expand Up @@ -652,7 +655,20 @@ fun GEN x th =
handle HOL_ERR _ => ERR "GEN" ""
end;

val GENL = itlist GEN
fun GENL vs th = let
val (asl,c) = sdest_thm th
in
if exists (fn v => var_occursl v asl) vs then
ERR "GENL" "variable occurs free in hypotheses"
else
make_thm
Count.Gen(tag th, asl,
list_mk_binder (SOME (prim_mk_const {Thy="bool", Name="!"}))
(vs,c),
GENL_prf(vs,th))
handle HOL_ERR _ => ERR "GENL" ""
end



(*---------------------------------------------------------------------------
Expand Down Expand Up @@ -1016,27 +1032,33 @@ fun Beta th =
handle HOL_ERR _ => ERR "Beta" "";


(*---------------------------------------------------------------------------*
* This rule behaves like a tactic: given a goal (reducing the rhs of thm), *
* it returns two subgoals (reducing the rhs of th1 and th2), together *
* with a validation (mkthm), that builds the normal form of t from the *
* normal forms of u and v. *
* NB: we do not have to typecheck the rator u, and we replaced the alpha *
* conversion test with pointer equality. *
* *
* |- u = u (th1) |- v = v (th2) *
* (thm) ... ... *
* A |- t = u v A' |- u = u' (th1') A'' |- v = v' (th2') *
* ---------------------------------------------------------------- *
* A u A' u A'' |- t = u' v' *
* *
* Could be implemented outside Thm as: *
* fun Mk_comb th = *
* let val {Rator,Rand} = dest_comb(rhs (concl th)) *
* fun mka th1 th2 = TRANS th (MK_COMB(th1,th2)) in *
* (REFL Rator, REFL Rand, mka) *
* end *
*---------------------------------------------------------------------------*)
(* --------------------------------------------------------------------------
This rule behaves like a tactic: given a goal (reducing the rhs of thm),
it returns two subgoals (reducing the rhs of th1 and th2), together
with a validation (mkthm), that builds the normal form of t from the
normal forms of u and v.
NB:
1. we do not have to typecheck the rator u,
2. there used to just be a pointer equality check in the Assert lines,
but this may cause unintended failures as gc-movement of values may
make things that are "morally" pointer-equal not compare equal.
The aconv test uses a pointer equality test as a fast-path option, so
this should still be quick most of the time.
|- u = u (th1) |- v = v (th2)
(thm) ... ...
A |- t = u v A' |- u = u' (th1') A'' |- v = v' (th2')
----------------------------------------------------------------
A u A' u A'' |- t = u' v'
Could be implemented outside Thm as:
fun Mk_comb th =
let val {Rator,Rand} = dest_comb(rhs (concl th))
fun mka th1 th2 = TRANS th (MK_COMB(th1,th2)) in
(REFL Rator, REFL Rand, mka)
end
--------------------------------------------------------------------------- *)

fun Mk_comb thm =
let val (lhs, rhs, ty) = Term.dest_eq_ty (concl thm)
Expand All @@ -1058,19 +1080,22 @@ fun Mk_comb thm =
end
handle HOL_ERR _ => ERR "Mk_comb" "";

(*---------------------------------------------------------------------------*
* |- u = u (th1) *
* (thm) ... *
* A |- t = \x.u A' |- u = u' (th1') *
* ---------------------------------------- x not in FV(A') *
* A u A' |- t = \x.u' *
* *
* Could be implemented outside Thm as: *
* fun Mk_abs th = *
* let val {Bvar,Body} = dest_abs(rhs (concl th)) in *
* (Bvar, REFL Body, (fn th1 => TRANS th (ABS Bvar th1))) *
* end *
*---------------------------------------------------------------------------*)
(* --------------------------------------------------------------------------
|- u = u (th1)
(thm) ...
A |- t = \x.u A' |- u = u' (th1')
---------------------------------------- x not in FV(A')
A u A' |- t = \x.u'
Could be implemented outside Thm as:
fun Mk_abs th =
let val {Bvar,Body} = dest_abs(rhs (concl th)) in
(Bvar, REFL Body, (fn th1 => TRANS th (ABS Bvar th1)))
end
See comment accompanying Mk_comb for discussion of use of aconv in first
Assert.
-------------------------------------------------------------------------- *)

fun Mk_abs thm =
let val (lhs, rhs, ty) = Term.dest_eq_ty (concl thm)
Expand Down Expand Up @@ -1366,10 +1391,52 @@ fun deductAntisym (th1 as THM(o1,a1,c1,p1)) (th2 as THM(o2,a2,c2,p2)) = let
in make_thm Count.Axiom (Tag.merge o1 o2, union_hyp a1' a2', mk_eq_nocheck bool c1 c2, deductAntisym_prf(th1,th2)) end

(* ----------------------------------------------------------------------
Disable compute primitive
Computing with first-order lisp-style values
---------------------------------------------------------------------- *)

fun compute {cval_terms, cval_type, num_type, char_eqns} _ _ =
raise ERR "compute" "disabled in opentheory kernel";
local
infix ##;
fun dest_code_eqn th =
case total ((List.null ## I) o dest_thm) th of
SOME (true,tm) => tm
| _ => raise ERR "compute" "code equation with hypotheses";
fun safe_mk_eq l r =
let
val tyl = type_of l
in
if tyl = type_of r then
Term.prim_mk_eq tyl l r
else
raise ERR "compute" "types of lhs and rhs disagree"
end;
val merge_tags = foldr (uncurry Tag.merge)
in
fun compute {cval_terms, cval_type, num_type, char_eqns} =
let
val tag0 = merge_tags empty_tag (List.map (tag o snd) char_eqns)
val char_eqns = List.map (I ## dest_thm) char_eqns
val _ = List.all (List.null o fst o snd) char_eqns
val tc0 = Compute.term_compute
{ cval_terms = cval_terms,
cval_type = cval_type,
num_type = num_type,
char_eqns = List.map (I ## snd) char_eqns }
in
fn code_eqs =>
let
val tag1 = merge_tags tag0 (List.map tag code_eqs)
val eqs = List.map dest_code_eqn code_eqs
val tc1 = tc0 eqs
in
fn tm =>
let
val tm' = tc1 tm
val eqn = safe_mk_eq tm tm'
in
make_thm Count.Compute (tag1, empty_hyp, eqn, compute_prf)
end
end
end;
end (*local *)

end (* Thm *)
3 changes: 3 additions & 0 deletions src/thm/otknl-thmsig.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ sig
include FinalThm
datatype proof =
Axiom_prf
| deleted_prf
| ABS_prf of term * thm
| ALPHA_prf of term * term
| AP_TERM_prf of term * thm
Expand All @@ -24,6 +25,7 @@ sig
| EQ_MP_prf of thm * thm
| EXISTS_prf of term * term * thm
| GEN_prf of term * thm
| GENL_prf of term list * thm
| GEN_ABS_prf of term option * term list * thm
| INST_TYPE_prf of (hol_type,hol_type)Lib.subst * thm
| INST_prf of (term,term)Lib.subst * thm
Expand All @@ -45,6 +47,7 @@ sig
| Mk_comb_prf of thm * thm * thm
| Specialize_prf of term * thm
| deductAntisym_prf of thm * thm
| compute_prf

val proof : thm -> proof
val delete_proof : thm -> unit
Expand Down

0 comments on commit 72a01e7

Please sign in to comment.