Hi,
I formalized cut elimination for a version of ordered logic (related to the
Lambek calculus) awhile ago, but never got it cleaned up to put anywhere.
It's available here:
https://github.com/tanyongkiam/15816/blob/master/ordered_logicScript.sml
The proof uses this method:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.173
It needed 1) names for each rule, and 2) a notion of size for proofs, which
aren't provided by default by Hol_reln. I got around this by 1) defining a
datatype of rulename identifiers and 2) adding a counter to each of the
rules.
I think 1) is what you are missing, and 2) is related to what you're trying
to define.
Note that if you just wanted 2), you can add it directly to the inductive
relation defining your rules as an additional argument instead of defining
a brand new relation.
On Thu, Jan 12, 2017 at 10:19 AM, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> Dear HOL users,
>
> Sorry for disturbing, but I have a long question about HOL.
>
> I’m trying to implement Lambek calculus in HOL with several deep theorems
> proved. This is my exam project on theorem proving. I found an existing
> work [1] based on Coq, so I think maybe I can migrate the existing work
> first, then add the proof for more theorems as my work. I have to say
> that, before mid December last year I have never proved anything
> successfully in HOL (although I have been reading HOL manuals & papers for
> several months), nor can I read Coq proof scripts, but I studied very much
> and today I got 1000 lines of HOL code as my implementation of Lambek
> Calculus [2].
>
> [1] https://github.com/coq-contribs/lambek
> [2] https://github.com/binghe/informatica-public/blob/
> master/lambek/LambekScript.sml
>
> (My question is at the end of this mail, people who doesn’t have time can
> skip this mail and save your time, thanks all the same!)
>
> Recall that, “when encoding any aspect of a logic, we must encode the
> basic syntactic expressions like atomic formulae, logical connectives, and
> formulae.” The Coq work has defined two concepts (Form and Term) which
> corresponds to syntactic categories of single words and sentences in Lambek
> calculus:
>
> """
> Inductive Form (Atoms : Set) : Set :=
> | At : Atoms -> Form Atoms
> | Slash : Form Atoms -> Form Atoms -> Form Atoms
> | Dot : Form Atoms -> Form Atoms -> Form Atoms
> | Backslash : Form Atoms -> Form Atoms -> Form Atoms.
>
> Inductive Term (Atoms:Set) : Set :=
> | OneForm : Form Atoms -> Term Atoms
> | Comma : Term Atoms -> Term Atoms -> Term Atoms."""
> """
>
> After reading "The HOL System TUTORIAL”carefully, especially “Chapter 6.
> Example: Combinatory Logic”, I think above definitions must be defining new
> datatypes, so I write down the following two Datatype definitions:
>
> """
> val _ = Datatype `Form = Atom 'a | Slash Form Form | Backslash Form Form |
> Dot Form Form`;
> val _ = Datatype `Term = OneForm ('a Form) | Comma Term Term`;
> """
>
> Now Coq scripts have gentzen styled sequent calculus defined in the same
> “Inductive” keyword: (I omitted some similar lines)
>
> """
> Variable E : gentzen_extension.
> Inductive gentzenSequent (Atoms : Set) : Term Atoms -> Form Atoms -> Set :=
> | Ax : forall A : Form Atoms, gentzenSequent (OneForm A) A
> | RightSlash :
> forall (Gamma : Term Atoms) (A B : Form Atoms),
> gentzenSequent (Comma Gamma (OneForm B)) A ->
> gentzenSequent Gamma (Slash A B)
> ...
> | CutRule :
> forall (Delta Gamma Gamma' : Term Atoms) (A C : Form Atoms),
> replace Gamma Gamma' (OneForm A) Delta ->
> gentzenSequent Delta A ->
> gentzenSequent Gamma C -> gentzenSequent Gamma' C
> | SequentExtension :
> forall (Gamma Gamma' T1 T2 : Term Atoms) (C : Form Atoms),
> E T1 T2 ->
> replace Gamma Gamma' T1 T2 ->
> gentzenSequent Gamma C -> gentzenSequent Gamma' C.
> """
>
> To me, this does’t look like a Datatype in HOL but Hol_reln, although it
> has three parameters:
>
> """
> val (gentzenSequent_rules, gentzenSequent_ind, _) = Hol_reln `
> (!(E:'a gentzen_extension) A. gentzenSequent E (OneForm A) A) /\ (*
> SeqAxiom *)
> (!E Gamma A B. (* RightSlash = SlashIntro *)
> gentzenSequent E (Comma Gamma (OneForm B)) A ==>
> gentzenSequent E Gamma (Slash A B)) /\
> ...
> (!E Delta Gamma Gamma' A C. (* CutRule *)
> replace Gamma Gamma' (OneForm A) Delta /\
> gentzenSequent E Delta A /\ gentzenSequent E Gamma C
> ==> gentzenSequent E Gamma' C) /\
> (!(E:'a gentzen_extension) Gamma Gamma' Delta Delta' C. (*
> SequentExtension *)
> replace Gamma Gamma' Delta Delta' /\ E Delta Delta' /\ gentzenSequent
> E Gamma C
> ==> gentzenSequent E Gamma' C)`;
>
> val [SeqAxiom, RightSlash, … ,CutRule, SequentExtension] = CONJ_LIST 9
> gentzenSequent_rules;
> """
>
> So far so good, actually I can easily migrate all theorems related to
> above Sequent calculus in one-to-one mapping, see the following theorem in
> Coq and HOL versions:
>
> “""
> (* Coq version *)
> Definition restructuring :
> forall (A B C : Form Atoms) (E : gentzen_extension),
> genExtends L_Sequent E ->
> gentzenSequent E (OneForm (Slash (Backslash A B) C))
> (Backslash A (Slash B C)).
>
> intros A B C E H.
> apply RightBackSlash.
> apply RightSlash.
> apply LextensionSimpl.
> assumption.
> apply CutRuleSimpl with (Dot A (Backslash A B)).
> apply RightDot.
> apply Ax.
> apply LeftSlashSimpl; apply Ax.
> apply application'.
> Defined.
>
> (* HOL version *)
> val restructuring = store_thm ("restructuring",
> ``!E A B C. extends L_Sequent E ==> gentzenSequent E (OneForm (Slash
> (Backslash A B) C))
> (Backslash A (Slash B C))``,
> REPEAT STRIP_TAC
>
> MATCH_MP_TAC RightBackslash
> MATCH_MP_TAC RightSlash
> MATCH_MP_TAC LextensionSimpl
> CONJ_TAC THEN1 (POP_ASSUM ACCEPT_TAC)
> MATCH_MP_TAC CutRuleSimpl
> EXISTS_TAC ``(Dot A (Backslash A B))``
> CONJ_TAC
>
> | [ MATCH_MP_TAC RightDot
>
> CONJ_TAC THEN1 REWRITE_TAC [SeqAxiom]
> MATCH_MP_TAC LeftSlashSimpl
> REWRITE_TAC [SeqAxiom],
>
> REWRITE_TAC [application'] ]);
> """
>
> The proof steps are exactly the same, the theorem sets used to prove above
> theorem is also the same. After “proving" 100+ such theorems in HOL, I
> felt that I’m going toward success to migrate all the Coq scripts, until I
> met the following strange definition: (it’s used in proving the
> cut-elimination theorem in Lambek’s sequent calculus)
>
> (* Recursive definition of the degree of a proof which is
> the max of the degree of its cut rules (the degree of a cut rule
> is the degree of the formula which is eliminated in the conclusion
> sequent )*)
>
> Fixpoint degreeProof (Atoms : Set) (Gamma : Term Atoms)
> (B : Form Atoms) (E : gentzen_extension) (p : gentzenSequent E Gamma B)
> {struct p} : nat :=
> match p with
> | Ax _ => 0
> | RightSlash _ _ _ H => degreeProof H
> | RightBackSlash _ _ _ H => degreeProof H
> | RightDot _ _ _ _ H1 H2 => max (degreeProof H1) (degreeProof H2)
> | LeftSlash _ _ _ _ _ _ R H1 H2 => max (degreeProof H1) (degreeProof H2)
> | LeftBackSlash _ _ _ _ _ _ R H1 H2 =>
> max (degreeProof H1) (degreeProof H2)
> | LeftDot _ _ _ _ _ R H => degreeProof H
> | CutRule _ _ _ A _ R H1 H2 =>
> max (max (degreeFormula A) (degreeProof H1)) (degreeProof H2)
> | SequentExtension _ _ _ _ _ E R H => degreeProof H
> end.
>
> It’s talking about the “proof” itself. it looks like a recursive function
> that I could define using HOL’s Define, but in HOL named like Ax,
> RightSlash, … are just names of theorems, and there’s no concept of “proof”
> defined so far, so I have no way to express the degree of a proof itself !!
> I’m stuck here…
>
> So my question is: how can I modify my previous definitions to be able to
> define “degreeProof” in HOL?
>
> P. S. I guess Coq is more powerful somehow, such that just "Shallow
> Embedding" would be enough to express theorems about proofs themselves. But
> in HOL some kinds of "Deep Embedding" is required, but I don’t know how to
> do it...
>
> ---
>
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
> ------------------------------------------------------------
> ------------------
> Developer Access Program for Intel Xeon Phi Processors
> Access to Intel Xeon Phi processor-based developer platforms.
> With one year of Intel Parallel Studio XE.
> Training and support from Colfax.
> Order your platform today. http://sdm.link/xeonphi
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Developer Access Program for Intel Xeon Phi Processors
Access to Intel Xeon Phi processor-based developer platforms.
With one year of Intel Parallel Studio XE.
Training and support from Colfax.
Order your platform today. http://sdm.link/xeonphi
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
