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 include "logic/connectives.ma".
16 include "logic/equality.ma".
18 record powerset (A: Type) : Type ≝ { char: A → Prop }.
20 notation "hvbox(2 \sup A)" non associative with precedence 45
21 for @{ 'powerset $A }.
23 interpretation "powerset" 'powerset A = (powerset A).
25 definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
27 notation "hvbox(a break ∈ b)" non associative with precedence 45
30 interpretation "mem" 'mem a S = (mem _ S a).
32 record axiom_set : Type ≝
35 C: ∀a:A. i a → 2 \sup A
38 inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
39 refl: ∀a:A. a ∈ U → covers A U a
40 | infinity: ∀a:A. ∀j: i ? a. coversl A U (C ? a j) → covers A U a
41 with coversl : (2 \sup A) → CProp ≝
42 iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
44 notation "hvbox(a break ◃ b)" non associative with precedence 45
45 for @{ 'covers $a $b }.
47 interpretation "covers" 'covers a U = (covers _ U a).
48 interpretation "coversl" 'covers A U = (coversl _ U A).
51 ∀A:axiom_set.∀U: 2 \sup A.∀P:A → CProp.
52 ∀H1:∀a:A. a ∈ U → P a.
53 ∀H2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
56 definition covers_elim ≝
57 λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
58 λH1:∀a:A. a ∈ U → a ∈ P.
59 λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P.
60 let rec aux (a:A) (p:a ◃ U) : a ∈ P ≝
61 match p return λaa.λ_.aa ∈ P with
63 | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
65 and auxl (V: 2 \sup A) (q: V ◃ U) : ∀b. b ∈ V → b ∈ P ≝
66 match q return λVV.λ_.∀b. b ∈ VV → b ∈ P with
67 [ iter VV f ⇒ λb.λr. aux b (f b r) ]
72 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
73 mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
75 notation "hvbox(a break ⋉ b)" non associative with precedence 45
78 interpretation "fish" 'fish a U = (fish _ U a).
80 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
81 (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
82 (H2: ∀a:A. a ∈ P → ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ y ∈ P) :
83 ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
89 [ ex_intro (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
91 [ conj (fHa: y ∈ C ? a j) (sHa: y ∈ P) ⇒
92 ex_intro A (λy.y ∈ C ? a j ∧ fish A U y) y
93 (conj ? ? fHa (fish_rec A U P H1 H2 y sHa))
97 theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
103 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
105 elim H using covers_elim;