matita/tests/dependent_injection.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 set "baseuri" "cic:/matita/tests/dependent_injection".
  16
  17 include "../legacy/coq.ma".
  18
  19 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  20 alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
  21 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
  22
  23 inductive ttree : Type → Type :=
  24    tempty: ttree nat
  25  | tnode : ∀A. ttree A → ttree A → ttree A.
  26
  27 (* CSC: there is an undecidable unification problem here:
  28     consider a constructor k : \forall x. f x -> i (g x)
  29     The head of the outtype of the injection MutCase should be (f ?1)
  30     such that (f ?1) unifies with (g d) [ where d is the Rel that binds
  31     the corresponding right parameter in the outtype ]
  32     Coq dodges the problem by generating an equality between sigma-types
  33     (that state the existence of a ?1 such that ...) *)
  34 theorem injection_test3:
  35  ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
  36  intros.
  37  destruct H.
  38  assumption.
  39 qed.
  40
  41 theorem injection_test3:
  42  ∀t,t'.
  43   tnode nat (tnode nat t t') tempty = tnode nat (tnode nat t' tempty) tempty →
  44    t = t'.
  45  intros;
  46  destruct H;
  47  assumption.
  48 qed.