matita/matita/tests/unifhint.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 record group : Type ≝ {
  16   gcarr :> Type;
  17   gmult : gcarr → gcarr → gcarr;
  18   gopp  : gcarr → gcarr;
  19   gunit : gcarr
  20 }.
  21
  22 interpretation "unif hints inverse" 'invert x = (gopp _ x).
  23 interpretation "unif hing times" 'times x y = (gmult _ x y).
  24 notation "𝟙" non associative with precedence 90 for @{ 'unit }.
  25 interpretation "unif hint unit" 'unit = (gunit _).
  26
  27 include "nat/nat.ma".
  28 include "list/list.ma".
  29
  30 inductive Expr : Type ≝
  31   | Evar : nat → Expr
  32   | Eopp : Expr → Expr
  33   | Eunit : Expr
  34   | Emult : Expr → Expr → Expr.
  35
  36 let rec sem (g : group) (e : Expr) (gamma : list (gcarr g)) on e : gcarr g ≝
  37   match e with
  38   [ Evar n ⇒ nth ? gamma 𝟙 n
  39   | Eopp x ⇒ (sem g x gamma) ^ -1
  40   | Eunit ⇒ 𝟙
  41   | Emult x y ⇒ (sem g x gamma) * (sem g y gamma)].
  42
  43 notation "〚term 19 x, term 19 g〛" non associative with precedence 90
  44 for @{ 'sem $x $g}.
  45 interpretation "unif hint sem" 'sem x g = (sem _ x g).
  46
  47 axiom P : ∀g:group. gcarr g → Prop.
  48 axiom tac : Expr → Expr.
  49 axiom start : ∀g,x,G.P g 〚x,G〛 → Prop.
  50
  51 notation > "ident a ≟ term 90 b term 20 c"
  52 non associative with precedence 90 for
  53 @{ let ${ident a} ≝ $b in $c }.
  54
  55 unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g).
  56            V ≟ 〚x,G〛
  57 (* ------------------------------------ *)
  58        〚Eopp x,G〛 = V^-1).
  59
  60
  61 unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g).
  62
  63        V1 ≟ 〚x,G〛        V2 ≟ 〚y,G〛
  64 (* ------------------------------------ *)
  65            〚Emult x y,G〛 = V1 * V2).
  66
  67 unification hint 0 (∀g:group.∀G:list (gcarr g).
  68
  69 (* ------------------------------------ *)
  70               〚Eunit,G〛 = 𝟙).
  71
  72 unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g.
  73
  74                    V ≟ x
  75 (* ------------------------------------ *)
  76           〚(Evar 0), (x :: G)〛 = V).
  77
  78 unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.
  79
  80                V ≟ 〚Evar n, G〛
  81 (* ------------------------------------ *)
  82        〚(Evar (S n)), (x :: G)〛 = V) .
  83
  84 (* Esempio banale di divergenza
  85 unification hint 0 (∀g:group.∀G:list (gcarr g).∀x.
  86      V ≟ 〚x,G〛
  87  ------------------------------------
  88       〚x,G〛 = V).
  89 *)
  90
  91 include "nat/plus.ma".
  92 unification hint 0 (∀x,y.S x + y = S (x + y)).
  93
  94 axiom T : nat → Prop.
  95 axiom F : ∀n,k.T (S (n + k)) → Prop.
  96 lemma diverge: ∀k,k1.∀h:T (? + k).F ? k1 h.
  97     ?+k    = S(?+k1)
  98     S?1 + k   S(?1+k1)
  99
 100 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)).
 101    start g ? ? h.
 102
 103 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)).
 104    start g ? ? h.
 105
 106    y == [| ?, x::? |]
 107
 108    〚Evar n, G〛
 109
 110
 111    int: 〚(Evar (S n)), (x :: G)〛 = 〚Evar n, G〛
 112                              nth (m) (G)          = 〚Evar n, G〛
 113
 114
 115 ∀x,Γ. [| B 0, x::Γ |] = x
 116 ∀n,y,Γ. [| B n, Γ |] = [| B (S n), y::Γ |]
 117 ∀e,f. [| Add e f, Γ |] = [| e, Γ |] + [| f, Γ |]
 118
 119
 120 x + x = [| ?1, ?2 |]
 121
 122 x = [| ?1,?2 |]
 123 ?1 ≝ B 0
 124 ?2 ≝ x::?3
 125
 126 x = [| ?4, y::x::?3 |]
 127
 128 [| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Γ |]
 129 x =?= [| B ?n, ?Γ |]
 130
 131
 132 x  =?=   E
 133
 134 x  =?=  ?,   ? =?= E