matita/matita/lib/lambda/subterms.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda/subst.ma".
  13
  14 inductive subterm : T → T → Prop ≝
  15   | appl : ∀M,N. subterm M (App M N)
  16   | appr : ∀M,N. subterm N (App M N)
  17   | lambdal : ∀M,N. subterm M (Lambda M N)
  18   | lambdar : ∀M,N. subterm N (Lambda M N)
  19   | prodl : ∀M,N. subterm M (Prod M N)
  20   | prodr : ∀M,N. subterm N (Prod M N)
  21   | sub_b : ∀M. subterm M (D M)
  22   | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P.
  23
  24 inverter subterm_myinv for subterm (?%).
  25
  26 lemma subapp: ∀S,M,N. subterm S (App M N) →
  27  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  28 #S #M #N #subH (@(subterm_myinv … subH))
  29   [#M1 #N1 #eqapp destruct /4/
  30   |#M1 #N1 #eqapp destruct /4/
  31   |3,4,5,6: #M1 #N1 #eqapp destruct
  32   |#M1 #eqapp destruct
  33   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqapp
  34    (cases (H2 eqapp))
  35     [* [* /3/ | #subN1 %1 %2 /2/ ]
  36     |#subN1 %2 /2/
  37     ]
  38   ]
  39 qed.
  40
  41 lemma sublam: ∀S,M,N. subterm S (Lambda M N) →
  42  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  43 #S #M #N #subH (@(subterm_myinv … subH))
  44   [1,2,5,6: #M1 #N1 #eqH destruct
  45   |3,4:#M1 #N1 #eqH destruct /4/
  46   |#M1 #eqH destruct
  47   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
  48    (cases (H2 eqH))
  49     [* [* /3/ | #subN1 %1 %2 /2/ ]
  50     |#subN1 %2 /2/
  51     ]
  52   ]
  53 qed.
  54
  55 lemma subprod: ∀S,M,N. subterm S (Prod M N) →
  56  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  57 #S #M #N #subH (@(subterm_myinv … subH))
  58   [1,2,3,4: #M1 #N1 #eqH destruct
  59   |5,6:#M1 #N1 #eqH destruct /4/
  60   |#M1 #eqH destruct
  61   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
  62    (cases (H2 eqH))
  63     [* [* /3/ | #subN1 %1 %2 /2/ ]
  64     |#subN1 %2 /2/
  65     ]
  66   ]
  67 qed.
  68
  69 lemma subd: ∀S,M. subterm S (D M) →
  70  S = M ∨ subterm S M.
  71 #S #M #subH (@(subterm_myinv … subH))
  72   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
  73   |#M1 #eqH destruct /2/
  74   |#M1 #N1 #P #sub1 #sub2 #_ #H #eqH
  75    (cases (H eqH)) /2/
  76     #subN1 %2 /2/
  77   ]
  78 qed.
  79
  80 lemma subsort: ∀S,n. ¬ subterm S (Sort n).
  81 #S #n % #subH (@(subterm_myinv … subH))
  82   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
  83   |#M1 #eqa destruct
  84   |/2/
  85   ]
  86 qed.
  87
  88 lemma subrel: ∀S,n. ¬ subterm S (Rel n).
  89 #S #n % #subH (@(subterm_myinv … subH))
  90   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
  91   |#M1 #eqa destruct
  92   |/2/
  93   ]
  94 qed.
  95
  96 theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) →
  97  ∀M. P M.
  98 #P #H #M (cut (P M ∧ (∀N. subterm N M → P N)))
  99   [2: * //]
 100 (elim M)
 101   [#n %
 102     [@H #N1 #subN1 @False_ind /2/
 103     |#N #subN1 @False_ind /2/
 104     ]
 105   |#n %
 106     [@H #N1 #subN1 @False_ind /2/
 107     |#N #subN1 @False_ind /2/
 108     ]
 109   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 110    (cut (∀N.subterm N (App M1 M2) → P N))
 111     [#N1 #subN1 (cases (subapp … subN1))
 112       [* [* // | @Hind1 ] | @Hind2 ]]
 113     #Hcut % /3/
 114   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 115    (cut (∀N.subterm N (Lambda M1 M2) → P N))
 116     [#N1 #subN1 (cases (sublam … subN1))
 117       [* [* // | @Hind1 ] | @Hind2 ]]
 118    #Hcut % /3/
 119   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 120    (cut (∀N.subterm N (Prod M1 M2) → P N))
 121     [#N1 #subN1 (cases (subprod … subN1))
 122       [* [* // | @Hind1 ] | @Hind2 ]]
 123    #Hcut % /3/
 124   |#M1 * #PM1 #Hind1
 125    (cut (∀N.subterm N (D M1) → P N))
 126     [#N1 #subN1 (cases (subd … subN1)) /2/]
 127    #Hcut % /3/
 128   ]
 129 qed.
 130
 131 let rec size M ≝
 132 match M with
 133   [Sort N ⇒ 1
 134   |Rel N ⇒ 1
 135   |App P Q ⇒ size P + size Q + 1
 136   |Lambda P Q ⇒ size P + size Q + 1
 137   |Prod P Q ⇒ size P + size Q + 1
 138   |D P ⇒ size P + 1
 139   ]
 140 .
 141
 142 (* axiom pos_size: ∀M. 1 ≤ size M. *)
 143
 144 theorem Telim_size: ∀P: T → Prop.
 145  (∀M. (∀N. size N < size M → P N) → P M) → ∀M. P M.
 146 #P #H #M (cut (∀p,N. size N = p → P N))
 147   [2: /2/]
 148 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size N0)) //
 149 qed.
 150
 151 (* size of subterms *)
 152
 153 lemma size_subterm : ∀N,M. subterm N M → size N < size M.
 154 #N #M #subH (elim subH) normalize //
 155 #M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
 156 qed.