Commit 0860fb7a authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Prove inconsistency of the "beta" axiom on the Coq side

parent 4b4c7cb4
Require Import String.
Require Import coq_obj.
Axiom beta : forall {A B} (f : Expr A -> Expr B) a,
Eval_meth (Make_meth f) a = f a.
Definition A := ["l" : Empty_type]%ty.
Definition a : Expr A := init A Istrue_true.
Definition H : A <: Empty_type := I.
Definition afalse : Expr Empty_type := empty_expression.
Definition atrue : Expr Empty_type :=
Expr_coerce Empty_type a H.
Definition not (e : Expr Empty_type) : Expr Empty_type
:=
match expr_type e with
| Empty_type => atrue
| _ => afalse
end.
Lemma not_true : not atrue = afalse.
Proof.
reflexivity.
Defined.
Lemma not_false : not afalse = atrue.
Proof.
reflexivity.
Defined.
Lemma true_is_not_false : ~ (atrue = afalse).
Proof.
intro H.
apply (f_equal expr_type) in H.
discriminate.
Defined.
Definition Hl : "l" domain A := PCons "l" (At_head "l" "l" nil eq_refl).
Eval compute in (A "l") Hl.
Definition obj_meth_extract (a : Obj A)
:=
preselect "l" a Hl.
Definition obj_select_2 l {A} (a : Obj A) (H : l domain A) (e : Expr A): Expr (assoc A l H).
Proof.
rewrite <- (obj_po_sub l a H).
exact (Eval_meth (preselect l a H) e).
Defined.
Definition select_2 l {A} (a : Expr A) (H : l domain A) (a' : Expr (expr_type a)) : Expr (assoc A l H).
Proof.
rewrite (assoc_subtype (expr_st a) l H).
exact (obj_select_2 l (expr_obj a) (domain_subtype (expr_st a) l H) a').
Defined.
Definition make_A (f : Expr A -> Expr Empty_type) : Expr A :=
pocons_3 ("l" = ς(x !: A) (f x))%meth
(init A Istrue_true).
Definition E (e : Expr A) : Expr Empty_type :=
not (select_2 "l"%string e Hl (Obj_to_expr (expr_obj e))).
Definition EE : Expr Empty_type :=
E (make_A E).
Eval compute in (A "l") Hl.
Lemma L1 : assoc_subtype (expr_st (make_A E)) "l" Hl = eq_refl Empty_type.
Proof.
reflexivity.
Defined.
Lemma string_eq_dec (l1 l2 : string) (H1 H2 : l1 = l2) : {H1 = H2} + {~ (H1 = H2)}.
Proof.
left.
apply (String_UIP.UIP l1 l2).
Defined.
Module String_eq_dec.
Definition U := ("l"%string = "l"%string).
Definition eq_dec := (string_eq_dec "l"%string "l"%string).
End String_eq_dec.
Module String_eq_UIP := Eqdep_dec.DecidableEqDep (String_eq_dec).
Lemma L2 : (String_UIP.UIP "l"%string "l"%string (@eq_refl string "l"%string) (@eq_refl string "l"%string)) = eq_refl.
Proof.
apply String_eq_UIP.UIP.
Defined.
Lemma L3 : obj_po_sub "l" (expr_obj (make_A E))
(domain_subtype (expr_st (make_A E)) "l"%string Hl) = eq_refl.
Proof.
simpl.
unfold obj_po_sub.
unfold obj_in_eq.
simpl.
unfold eq_ind_r.
unfold eq_sym.
simpl.
rewrite L2.
reflexivity.
Defined.
Lemma L4 : obj_po_sub "l" (obj_init A Istrue_true)
(PCons "l" (At_head "l" "l" nil eq_refl)) = eq_refl.
Proof.
exact L3.
Defined.
Lemma L5 : expr_st (init A Istrue_true) = subtype_refl A.
Proof.
reflexivity.
Defined.
Lemma L6 : Obj_to_expr (expr_obj (make_A E)) = make_A E.
Proof.
reflexivity.
Defined.
Lemma E_is_not_E : EE = not EE.
Proof.
unfold EE.
unfold E at 1.
f_equal.
unfold select_2.
rewrite L1.
unfold eq_rect_r.
unfold eq_sym.
unfold eq_rect.
unfold obj_select_2.
rewrite L3.
unfold eq_rect.
rewrite L6.
simpl.
unfold eq_rect_r, eq_sym, eq_rect.
simpl.
unfold eq_rec_r, eq_sym, eq_rec.
simpl.
rewrite L4.
rewrite beta.
rewrite beta.
reflexivity.
Defined.
Definition ground (e : Expr Empty_type) :=
match expr_type e with
| Empty_type => True
| _ => False
end.
Lemma ground_not_1 e : ground e -> ~(ground (not e)).
Proof.
unfold ground, not.
case (expr_type e); simpl; intuition.
Defined.
Lemma ground_not_2 e : {ground (e)} + {ground (not e)}.
Proof.
unfold ground, not.
case (expr_type e); simpl; intuition.
Defined.
Lemma E_not_ground : ~ ground EE.
Proof.
intro H.
assert (H1 : ground EE) by exact H.
rewrite E_is_not_E in H.
exact (ground_not_1 EE H1 H).
Defined.
Lemma absurd : False.
destruct (ground_not_2 EE) as [g | g].
- exact (E_not_ground g).
- rewrite <- E_is_not_E in g.
exact (E_not_ground g).
Defined.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment