helm/software/matita/contribs/formal_topology/bin/combinations.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 "datatypes/bool.ma".
  16 include "datatypes/constructors.ma".
  17
  18 inductive ct: Type ≝
  19    C: option mmt → ct
  20 with mmt: Type ≝
  21    M: option ct → mmt
  22  | MM: option ct → mmt.
  23
  24 inductive t: Type ≝
  25    E: t
  26  | CT: ct → t
  27  | MMT: mmt → t.
  28
  29 (*
  30 let rec ct_rect' (P1: ct → Type) (P2: mmt → Type) (f1: ∀w: mmt. P2 w → P1 (C w)) (f2: P1 E) (f3: ∀w: ct. P1 w → P2 (M1 w)) (f4: ∀w: ct. P1 w → P2 (M2 w)) (f5: P2 E') (w:ct) on w : P1 w ≝
  31  match w return λw. P1 w with
  32   [ C w' ⇒ f1 w' (mmt_rect' P1 P2 f1 f2 f3 f4 f5 w')
  33   | E ⇒ f2 ]
  34 and mmt_rect' (P1: ct → Type) (P2: mmt → Type) (f1: ∀w: mmt. P2 w → P1 (C w)) (f2: P1 E) (f3: ∀w: ct. P1 w → P2 (M1 w)) (f4: ∀w: ct. P1 w → P2 (M2 w)) (f5: P2 E') (w:mmt) on w : P2 w ≝
  35  match w return λw. P2 w with
  36   [ M1 w' ⇒ f3 w' (ct_rect' P1 P2 f1 f2 f3 f4 f5 w')
  37   | M2 w' ⇒ f4 w' (ct_rect' P1 P2 f1 f2 f3 f4 f5 w')
  38   | E' ⇒ f5 ].
  39 *)
  40
  41 definition c: t → t ≝
  42  λw.
  43   match w with
  44    [ E ⇒ CT (C (None ?))
  45    | CT _ ⇒ w
  46    | MMT w' ⇒ CT (C (Some ? w')) ].
  47
  48 definition m: t → t ≝
  49  λw.
  50   match w with
  51    [ E ⇒ MMT (M (None ?))
  52    | CT w' ⇒ MMT (M (Some ? w'))
  53    | MMT w' ⇒
  54       match w' with
  55        [ M w'' ⇒ MMT (MM w'')
  56        | MM w'' ⇒ MMT (M w'') ]].
  57
  58 definition i: t → t ≝ λw.w.
  59
  60 inductive leq: t → t → Prop ≝
  61    leq0: ∀w. leq w w
  62  | leq1: ∀w1,w2,w3. leq w1 w2 → leq w2 w3 → leq w1 w3
  63  | leq2: ∀w1,w2. leq w1 w2 → leq w1 (c w2)
  64  | leq3: ∀w1,w2. leq w1 w2 → leq (c (c w1)) (c w2)
  65  | leq4: ∀w1,w2. leq w1 w2 → leq (c w1) (c w2)
  66  | leq5: ∀w1,w2. leq w1 w2 → leq (m w2) (m (m (m w1)))
  67  | leq6: ∀w1,w2. leq w1 w2 → leq w1 (m (m w2))
  68  | leq7: ∀w1,w2. leq w1 w2 → leq (m w2) (m w1).
  69
  70 theorem ok: ∀w1,w2. leq w1 w2 → leq w2 w1 → w1 = w2.
  71
  72
  73 inductive leq: t → t → Prop ≝
  74    leq1: leq E (MMT (MM (None ?)))
  75  | leq2: leq E (CT (C (None ?)))
  76  | leq3: ∀w. leq (MMT w) (CT (C (Some ? w)))
  77  | leq4: ∀w. leq (CT w) (MMT (MM (Some ? w))).
  78
  79 theorem leq_ok: ∀w1,w2. leq w1 w2 → leq w2 w1 → w1 = w2.
  80  intros 3; elim H;
  81   [ reflexivity;
  82   | elim H5 in H1 H2 H3 H4 ⊢ %;
  83      [ reflexivity;
  84      | rewrite > H4; try assumption; try autobatch; [ apply H2;
  85        try autobatch; ] intro; [ transitivity t3;
  86         [ apply H2; try autobatch; ] intros;
  87      |
  88      |
  89
  90 definition LEQ ≝ λw1,w2:t. bool.
  91
  92 definition leq: t → t → bool.
  93  intro w1; change with (∀w2. LEQ w1 w2); cases w1 (w1'); clear w1;
  94   [ apply (ct_rect' ? (λw1.∀w2.LEQ (MMT w1) w2) ????? w1'); simplify; clear w1';
  95      [
  96      |
  97
  98  intros (w1 w2); change with (LEQ w1 w2);
  99  cases w1 (w1' w1'); [ apply (ct_rect' ??????? w1'); cases w1'; cases w2 (w2' w2'); cases w2';
 100   [
 101
 102 let rec leq (w1: t) (w2: t) : bool ≝
 103  match w1 with
 104   [ CT w1' ⇒
 105      match w1' with
 106       [ E ⇒ match w2 with [CT w2' ⇒
 107