helm/software/matita/tests/unifhint_simple.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 inductive Expr (g : group) : Type ≝
  28   | Evar : gcarr g → Expr g
  29   | Eopp : Expr g → Expr g
  30   | Eunit : Expr g
  31   | Emult : Expr g → Expr g → Expr g.
  32
  33 let rec sem (g : group) (e : Expr g) on e : gcarr g ≝
  34   match e with
  35   [ Evar x ⇒ x
  36   | Eopp x ⇒ (sem g x) ^ -1
  37   | Eunit ⇒ 𝟙
  38   | Emult x y ⇒ (sem g x) * (sem g y)].
  39
  40 notation "〚x〛" non associative with precedence 90 for @{ 'sem $x }.
  41 interpretation "unif hint sem" 'sem x = (sem _ x).
  42
  43 axiom P : ∀g:group. gcarr g → Prop.
  44 axiom tac : ∀g:group. Expr g → Expr g.
  45 axiom start : ∀g,x.P g 〚x〛 → Prop.
  46
  47
  48 include "logic/equality.ma".
  49
  50 notation "@ t" non associative with precedence 90 for @{ (λx.x) $t }.
  51
  52 unification hint (∀g:group.∀x:g. 〚Evar ? x〛 = x).
  53 unification hint (∀g:group.∀x. 〚Eopp g x〛 = (@〚x〛) ^-1).
  54 unification hint (∀g:group.∀x,y. 〚Emult g x y〛 = (@〚x〛) * (@〚y〛)).
  55
  56 lemma test : ∀g:group.∀x,y:g. ∀h:P ? (x * (x^-1 * y)). start g ? h.
  57
  58
  59
  60 ∀x,Γ. [| B 0, x::Γ |] = x
  61 ∀n,y,Γ. [| B n, Γ |] = [| B (S n), y::Γ |]
  62 ∀e,f. [| Add e f, Γ |] = [| e, Γ |] + [| f, Γ |]
  63
  64
  65 x + x = [| ?1, ?2 |]
  66
  67 x = [| ?1,?2 |]
  68 ?1 ≝ B 0
  69 ?2 ≝ x::?3
  70
  71 x = [| ?4, y::x::?3 |]
  72
  73 [| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Γ |]
  74 x =?= [| B ?n, ?Γ |]
  75
  76
  77 x  =?=   E
  78
  79 x  =?=  ?,   ? =?= E