1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/test/coercions_propagation/".
17 include "logic/connectives.ma".
18 include "nat/orders.ma".
19 alias num (instance 0) = "natural number".
21 inductive sigma (A:Type) (P:A → Prop) : Type ≝
22 sigma_intro: ∀a:A. P a → sigma A P.
24 interpretation "sigma" 'exists \eta.x =
25 (cic:/matita/test/coercions_propagation/sigma.ind#xpointer(1/1) _ x).
27 definition inject ≝ λP.λa:nat.λp:P a. sigma_intro ? P ? p.
29 coercion cic:/matita/test/coercions_propagation/inject.con 0 1.
31 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ sigma_intro w _ ⇒ w].
33 coercion cic:/matita/test/coercions_propagation/eject.con.
35 alias num (instance 0) = "natural number".
37 theorem test: ∃n. 0 ≤ n.
38 apply (S O : ∃n. 0 ≤ n).
42 theorem test2: nat → ∃n. 0 ≤ n.
43 apply ((λn:nat. 0) : nat → ∃n. 0 ≤ n);
47 theorem test3: (∃n. 0 ≤ n) → nat.
48 apply ((λn:nat.n) : (∃n. 0 ≤ n) → nat).
51 theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
52 apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
58 theorem test5: nat → ∃n. 0 ≤ n.
61 (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?]