1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
(* Check pattern-unification on evars in apply unification *)
Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'.
Axiom copy : forall tau:Type, tau -> tau -> Prop.
Axiom copyr : forall tau:Type, tau -> tau -> Prop.
Axiom copyf : forall tau:Type, tau -> tau -> Prop.
Axiom eq : forall tau:Type, tau -> tau -> Prop.
Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop.
Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'.
Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'),
(forall x:tau, copyr tau x x->copy tau' (t x) (t' x))
->copy (tau->tau') t t'.
Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'.
Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'),
copyr (tau->tau') t t'
->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)).
Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'.
Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'),
copyr (tau->tau') t t'
->(forall x y:tau, forall z1 z2:tau',
(copy tau x y)->
(subst tau tau' t x z1)->
(subst tau tau' t' y z2)->
copyf tau' z1 z2).
Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau',
( ((subst tau tau' t q t') /\ (eq tau' t' r))
->eq tau' (app tau tau' t q) r).
Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t'))
->eq tau' r (app tau tau' t q).
Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r))
->subst tau tau' t q r.
Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
Ltac Subst := apply substcopy;intros;EtaLong.
Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.
Theorem church0: forall i:Type, exists X:(i->i)->i->i,
copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
intros.
esplit.
EtaLong.
eapply eqappd;split.
Subst.
apply copyf_atom.
Show Existentials.
apply H1.
|
