helm/software/matita/nlibrary/logic/destruct_bb.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 "nat/nat.ma".
  16 include "list/list.ma".
  17
  18 inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
  19 | il_s : ∀n.T n → index_list T n n
  20 | il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
  21
  22 lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
  23                 ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
  24 intros 5;elim i
  25 [destruct;apply il_s;apply f;assumption
  26 |apply il_c
  27  [apply f;rewrite > H;assumption
  28  |apply f1
  29   [rewrite > H;reflexivity
  30   |assumption]]]
  31 qed.
  32
  33 definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
  34   λT0:Type.λT1:T0 → Type.
  35   λa0,b0:T0.
  36   λe0:a0 = b0.
  37   λso:T1 a0.
  38   eq_rect' ?? (λy,p.T1 y) so ? e0.
  39   *)
  40
  41 include "logic/equality.ma".
  42
  43 ndefinition R1 ≝ eq_rect_Type0.
  44 ndefinition R2 :
  45   ∀T0:Type[0].
  46   ∀a0:T0.
  47   ∀T1:∀x0:T0. a0=x0 → Type[0].
  48   ∀a1:T1 a0 (refl ? a0).
  49   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
  50   ∀b0:T0.
  51   ∀e0:a0 = b0.
  52   ∀b1: T1 b0 e0.
  53   ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
  54   ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
  55 #T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
  56 napply (eq_rect_Type0 ????? e1);
  57 napply (R1 ?? ? ?? e0);
  58 napply H;
  59 nqed.
  60
  61 ndefinition R3 :
  62   ∀T0:Type[0].
  63   ∀a0:T0.
  64   ∀T1:∀x0:T0. a0=x0 → Type[0].
  65   ∀a1:T1 a0 (refl ? a0).
  66   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
  67   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  68   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
  69       ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
  70   ∀b0:T0.
  71   ∀e0:a0 = b0.
  72   ∀b1: T1 b0 e0.
  73   ∀e1:R1 ? a0 ? a1 ? e0 = b1.
  74   ∀b2: T2 b0 e0 b1 e1.
  75   ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
  76   ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
  77 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
  78 napply (eq_rect_Type0 ????? e2);
  79 napply (R2 ?? ? ??? e0 ? e1);
  80 napply H;
  81 nqed.