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      ])).