-let rec is_dummy M ≝
-match M with
- [D P ⇒ true
- |_ ⇒ false
- ].
-
-let rec is_lambda M ≝
-match M with
- [Lambda P Q ⇒ true
- |_ ⇒ false
- ].
-
-theorem is_dummy_to_exists: ∀M. is_dummy M = true →
-∃N. M = D N.
-#M (cases M) normalize
- [1,2: #n #H destruct|3,4,5: #P #Q #H destruct
- |#N #_ @(ex_intro … N) //
- ]
-qed.
-
-theorem is_lambda_to_exists: ∀M. is_lambda M = true →
-∃P,N. M = Lambda P N.
-#M (cases M) normalize
- [1,2,6: #n #H destruct|3,5: #P #Q #H destruct
- |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
- ]
-qed.
-
-inductive pr : T →T → Prop ≝
- | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 →
- pr (App (Lambda P M) N) (M1[0 ≝ N1])
- | dapp: ∀M,N,P. pr (App M N) P →
- pr (App (D M) N) (D P)
- | dlam: ∀M,N,P. pr (Lambda M N) P → pr (Lambda M (D N)) (D P)
- | none: ∀M. pr M M
- | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1)
- | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 →
- pr (Lambda P M) (Lambda P1 M1)
- | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 →
- pr (Prod P M) (Prod P1 M1)
- | d: ∀M,M1. pr M M1 → pr (D M) (D M1).
-
-lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n.
-#M #n #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |//
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
-#M #n #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |//
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
-#M #N #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#R #eqR <eqR #_ @(ex_intro … N) /2/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
- ]
-qed.
-
-lemma prApp_not_dummy_not_lambda:
-∀M,N,P. pr (App M N) P → is_dummy M = false → is_lambda M = false →
-∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
-#M #N #P #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #_ #H1 destruct
- |#M1 #N1 #P1 #_ #_ #H destruct #_ #H1 destruct
- |#M #N #P1 #_ #_ #H destruct
- |#Q #eqProd #_ #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
- |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ #_ destruct
- @(ex_intro … N1) @(ex_intro … N2) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prApp_D:
-∀M,N,P. pr (App (D M) N) P →
- (∃Q. (P = D Q ∧ pr (App M N) Q)) ∨
- (∃M1,N1.(P = (App (D M1) N1) ∧ pr M M1 ∧ pr N N1)).
-#M #N #P #prH (inversion prH)
- [#R #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M1 #N1 #P1 #pr1 #_ #H destruct #eqP
- @or_introl @(ex_intro … P1) /2/
- |#M #N #P1 #_ #_ #H destruct
- |#R #eqR #_ @or_intror @(ex_intro … M) @(ex_intro … N) /3/
- |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
- cases (prD … pr1) #S * #eqN1 >eqN1 #pr3
- @or_intror @(ex_intro … S) @(ex_intro … N2) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prApp_lambda:
-∀Q,M,N,P. pr (App (Lambda Q M) N) P →
-∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
- (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
-#Q #M #N #P #prH (inversion prH)
- [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_
- @(ex_intro … M1) @(ex_intro … N1) /4/
- |#M1 #N1 #P1 #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#R #eqR #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/
- |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
- @(ex_intro … N1) @(ex_intro … N2) /4/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prLambda_not_dummy: ∀M,N,P. pr (Lambda M N) P → is_dummy N = false →
-∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
-#M #N #P #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct #_ #eqH destruct
- |#Q #eqProd #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 #_ destruct
- @(ex_intro … Q1) @(ex_intro … S1) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prLambda_dummy: ∀M,N,P. pr (Lambda M (D N)) P →
- (∃M1,N1. P = Lambda M1 (D N1) ∧ pr M M1 ∧ pr N N1) ∨
- (∃Q. (P = D Q ∧ pr (Lambda M N) Q)).
-#M #N #P #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#M1 #N1 #P1 #prM #_ #eqlam destruct #H @or_intror
- @(ex_intro … P1) /3/
- |#Q #eqLam #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
- cases (prD …pr2) #S2 * #eqS1 #pr3 >eqS1 @or_introl
- @(ex_intro … Q1) @(ex_intro … S2) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
-(∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1)) ∨
-(∃N1,Q. (N=D N1) ∧ (P = (D Q) ∧ pr (Lambda M N1) Q)).
-#M #N #P #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#M1 #N1 #P1 #prM1 #_ #eqlam #eqP destruct @or_intror
- @(ex_intro … N1) @(ex_intro … P1) /3/
- |#Q #eqProd #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct @or_introl
- @(ex_intro … Q1) @(ex_intro … S1) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
- ]
-qed.
-
-lemma prProd: ∀M,N,P. pr (Prod M N) P →
-∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
-#M #N #P #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#M #N #P1 #_ #_ #H destruct
- |#Q #eqProd #_ @(ex_intro … M) @(ex_intro … N) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
- @(ex_intro … Q1) @(ex_intro … S1) /3/
- |#M #N #_ #_ #H destruct
- ]