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 "datatypes/bool.ma".
16 include "datatypes/constructors.ma".
22 | MM: option ct → mmt.
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')
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')
46 | MMT w' ⇒ CT (C (Some ? w')) ].
51 [ E ⇒ MMT (M (None ?))
52 | CT w' ⇒ MMT (M (Some ? w'))
55 [ M w'' ⇒ MMT (MM w'')
56 | MM w'' ⇒ MMT (M w'') ]].
58 definition i: t → t ≝ λw.w.
60 inductive leq: t → t → Prop ≝
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).
70 theorem ok: ∀w1,w2. leq w1 w2 → leq w2 w1 → w1 = w2.
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))).
79 theorem leq_ok: ∀w1,w2. leq w1 w2 → leq w2 w1 → w1 = w2.
82 | elim H5 in H1 H2 H3 H4 ⊢ %;
84 | rewrite > H4; try assumption; try autobatch; [ apply H2;
85 try autobatch; ] intro; [ transitivity t3;
86 [ apply H2; try autobatch; ] intros;
90 definition LEQ ≝ λw1,w2:t. bool.
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';
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';
102 let rec leq (w1: t) (w2: t) : bool ≝
106 [ E ⇒ match w2 with [CT w2' ⇒