]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/formal_topology.ma
update in basic_2
[helm.git] / matitaB / matita / tests / formal_topology.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 include "logic/connectives.ma".
16
17 coinductive fish (A:Type) (i: A → Type) (C: ∀a:A.i a → A → Prop) (U: A → Prop)
18                : A → Prop
19
20  mk_foo: ∀a:A. (U a ∧ ∀j: i a. ∃y: A. C a j y ∧ fish A i C U y) → fish A i C U a.
21
22 let corec fish_rec (A:Type) (i: A → Type) (C: ∀a:A.i a → A → Prop) (U: A → Prop)
23  (P: A → Prop) (H1: ∀a:A. P a → U a)
24   (H2: ∀a:A. P a → ∀j: i a. ∃y: A. C a j y ∧ P y) :
25    ∀a:A. ∀p: P a. fish A i C U a ≝
26  λa,p.
27   mk_foo A i C U a
28    (conj ? ? (H1 ? p)
29    (λj: i a.
30     match H2 a p j with
31      [ ex_intro (y: A) (Ha: C a j y ∧ P y) ⇒
32         match Ha with
33          [ conj (fHa: C a j y) (sHa: P y) ⇒
34             ex_intro A (λy.C a j y ∧ fish A i C U y) y
35              (conj ? ? fHa (fish_rec A i C U P H1 H2 y sHa))
36          ]
37      ])).