From 3c6725a5969f4321ba95bb01211b4c23cc8341dc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 27 Sep 2007 14:48:14 +0000 Subject: [PATCH] added some notation --- matita/contribs/LOGIC/CLE/defs.ma | 14 ++++++++++++ matita/contribs/LOGIC/PEq/defs.ma | 35 +++++++++++++++++++++++++++++ matita/contribs/LOGIC/PNF/defs.ma | 12 +++++----- matita/contribs/LOGIC/PRed/defs.ma | 4 ++++ matita/contribs/LOGIC/PRed/wlt.ma | 29 ++++++++++++++++++++++++ matita/contribs/LOGIC/Track/pred.ma | 2 +- matita/contribs/LOGIC/WLT/defs.ma | 34 ++++++++++++++++++++++++++++ 7 files changed, 124 insertions(+), 6 deletions(-) create mode 100644 matita/contribs/LOGIC/PEq/defs.ma create mode 100644 matita/contribs/LOGIC/PRed/wlt.ma create mode 100644 matita/contribs/LOGIC/WLT/defs.ma diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma index 31bd7694e..a714a0488 100644 --- a/matita/contribs/LOGIC/CLE/defs.ma +++ b/matita/contribs/LOGIC/CLE/defs.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + set "baseuri" "cic:/matita/LOGIC/CLE/defs". (* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS diff --git a/matita/contribs/LOGIC/PEq/defs.ma b/matita/contribs/LOGIC/PEq/defs.ma new file mode 100644 index 000000000..eabbfb8a6 --- /dev/null +++ b/matita/contribs/LOGIC/PEq/defs.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/PEq/defs". + +(* EQUALITY PREDICATE FOR PROOFS IN CONTEXT +*) + +include "datatypes/Context.ma". + +inductive PEq (Q1:Context) (p1:Proof) (Q2:Context) (p2:Proof): Prop \def + | peq_intro: Q1 = Q2 \land p1 = p2 \to PEq Q1 p1 Q2 p2 +. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation + "leibniz equality between proofs in context" + 'eq2 x1 y1 x2 y2 = + (cic:/matita/LOGIC/PEq/defs/PEq.ind#xpointer(1/1) x1 y1 x2 y2) +. + +notation "hvbox([a1,b1] break = [a2,b2])" + non associative with precedence 45 +for @{ 'eq2 $a1 $b1 $a2 $b2 }. diff --git a/matita/contribs/LOGIC/PNF/defs.ma b/matita/contribs/LOGIC/PNF/defs.ma index feea35b43..4f11e8c56 100644 --- a/matita/contribs/LOGIC/PNF/defs.ma +++ b/matita/contribs/LOGIC/PNF/defs.ma @@ -14,12 +14,14 @@ set "baseuri" "cic:/matita/LOGIC/PNF/defs". -(* NORMAL FORM PREDICATE FOR PARALLEL REDUCTION +(* NORMAL FORM PREDICATE FOR PROOFS IN CONTEXT + For cut elimination *) +include "PEq/defs.ma". include "PRed/defs.ma". -(* -inductive PNF: Proof \to Prop \def - | pnf: \forall p. (\forall q. p => q \to p = q) \to PNF p + +inductive PNF (P:Context) (p:Proof): Prop \def + | pnf: (\forall q,Q,S. [P, p, S] => [Q, q, S] \to [P, p] = [Q, q]) \to + PNF P p . -*) diff --git a/matita/contribs/LOGIC/PRed/defs.ma b/matita/contribs/LOGIC/PRed/defs.ma index 51aaa94b2..85a4c3bf9 100644 --- a/matita/contribs/LOGIC/PRed/defs.ma +++ b/matita/contribs/LOGIC/PRed/defs.ma @@ -57,3 +57,7 @@ interpretation 'parred3 x1 y1 z1 x2 y2 z2 = (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x1 y1 z1 x2 y2 z2) . + +notation "hvbox([a1,b1,c1] break => [a2,b2,c2])" + non associative with precedence 45 +for @{ 'parred3 $a1 $b1 $c1 $a2 $b2 $c2 }. diff --git a/matita/contribs/LOGIC/PRed/wlt.ma b/matita/contribs/LOGIC/PRed/wlt.ma new file mode 100644 index 000000000..3e7d727ed --- /dev/null +++ b/matita/contribs/LOGIC/PRed/wlt.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/PRed/wlt". + +(**) + +include "PEq/defs.ma". +include "PRed/defs.ma". +include "WLT/defs.ma". +(* +theorem pred_wlt: \forall p1,p2,Q1,Q2,S. + [Q1, p1, S] => [Q2, p2, S] \to \lnot [Q1, p1] = [Q2, p2] \to + [Q2, p2] < [Q1, p1]. + intros 6; elim H; clear H; + [ unfold Not in H1; lapply linear depth = 1 H1; + [ decompose | autobatch ] +*) diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma index c7f6198f9..f9c172813 100644 --- a/matita/contribs/LOGIC/Track/pred.ma +++ b/matita/contribs/LOGIC/Track/pred.ma @@ -19,7 +19,7 @@ set "baseuri" "cic:/matita/LOGIC/Track/pred". include "Track/inv.ma". include "PRed/defs.ma". -theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. PRed Q1 p1 S1 Q2 p2 S2 \to +theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. [Q1, p1, S1] => [Q2, p2, S2] \to Track Q1 p1 S1 \to Track Q2 p2 S2. intros 7; elim H; clear H Q1 Q2 p1 p2 S1 S2; [ autobatch diff --git a/matita/contribs/LOGIC/WLT/defs.ma b/matita/contribs/LOGIC/WLT/defs.ma new file mode 100644 index 000000000..5a844a60a --- /dev/null +++ b/matita/contribs/LOGIC/WLT/defs.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/WLT/defs". + +(* ORDER RELATION BETWEEN PROOFS IN CONTEXT +*) + +include "Weight/defs.ma". + +inductive WLT (Q1:Context) (p1:Proof) (Q2:Context) (p2:Proof): Prop \def + | wlt_intro: \forall m,m1. Weight m Q1 p1 m1 \to + \forall m2. Weight m Q2 p2 m2 \to + m1 < m2 \to WLT Q1 p1 Q2 p2 +. + +interpretation "order relation between proofs in context" + 'lt2 x1 y1 x2 y2 = + (cic:/matita/LOGIC/WLT/defs/WLT.ind#xpointer(1/1) x1 y1 x2 y2). + +notation "hvbox([a1, b1] break \lt [a2, b2])" + non associative with precedence 45 +for @{ 'lt2 $a1 $b1 $a2 $b2 }. -- 2.39.2