From f4d8fe802ca50904dafdf680a199253d65a4a84c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2009 14:42:15 +0000 Subject: [PATCH] nice notation for hints! --- .../matita/nlibrary/hints_declaration.ma | 51 +++++++++++++++++-- 1 file changed, 47 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma index 5c189f63a..b826d2e76 100644 --- a/helm/software/matita/nlibrary/hints_declaration.ma +++ b/helm/software/matita/nlibrary/hints_declaration.ma @@ -12,7 +12,44 @@ (* *) (**************************************************************************) +(* + +Notation for hint declaration +============================== + +The idea is to write a context, with abstraction first, then +recursive calls (let-in) and finally the two equivalent terms. +The context can be empty. Note the ; to begin the second part of +the context (necessary even if the first part is empty). + + unification hint PREC \coloneq + ID : TY, ..., ID : TY + ; ID \equest T, ..., ID \equest T + \vdash T1 \equiv T2 + +With unidoce and some ASCII art it looks like the following: + + unification hint PREC ≔ ID : TY, ..., ID : TY; + ID ≟ T, ..., ID ≟ T + (*---------------------*) ⊢ + T1 ≡ T2 + +*) + +notation > "≔ (list0 ( ident x : T ) sep ,) opt (; (list1 (ident U ≟ term 90 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py" + with precedence 90 + for @{ ${ fold right + @{ ${ default + @{ ${ fold right + @{ 'hint_decl $Px $Py } + rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } } + @{ 'hint_decl $Px $Py } + } + } + rec acc @{ ∀${ident x}:$T.$acc } } }. + include "logic/pts.ma". + ndefinition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop. ndefinition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop. ndefinition hint_declaration_Type2 ≝ λa,b:Type[1].Prop. @@ -20,13 +57,19 @@ ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop. ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop. ndefinition hint_declaration_CProp2 ≝ λa,b:CProp[1].Prop. -notation > "≔ (list0 (ident x : T ) sep ,) ⊢ term 19 Px ≡ term 19 Py" - with precedence 90 - for @{ ${ fold right @{'hint_decl $Px $Py} rec acc @{ ∀${ident x}:$T.$acc } } }. - interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b). interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b). interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b). interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b). interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b). interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b). + +(* little test +naxiom A : Type[0]. +naxiom C : A → A → Type[0]. +ndefinition D ≝ C. +alias symbol "hint_decl" = "hint_decl_Type1". +unification hint 0 ≔ + X : A, Y : A ; Z ≟ X, W ≟ Y ⊢ C X Y ≡ D Z W. + +*) -- 2.39.2