]> matita.cs.unibo.it Git - helm.git/blob - matita/tests/dependent_injection.ma
reorganization of the whole story, the root dir contains the algebraic structure
[helm.git] / 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.