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

Decidability of subtyping proved

parent f0fbd3f7
......@@ -34,6 +34,34 @@ Proof.
reflexivity.
Defined.
Lemma Istrue_case b : {Istrue b} + {Istrue (negb b)}.
Proof.
case b; [ left | right ]; exact Istrue_true.
Defined.
Lemma Istrue_case_not_right b c:
Istrue (match Istrue_case b with left H => c H | right _ => false end) ->
Istrue b.
Proof.
destruct b.
- intro.
exact Istrue_true.
- unfold Istrue_case.
intro.
assumption.
Defined.
Lemma Istrue_case_not_right_fun b c H:
Istrue (c (Istrue_case_not_right b c H)).
Proof.
generalize H.
destruct b.
- simpl. intro. assumption.
- unfold Istrue_case.
intro H2.
inversion H2.
Defined.
Definition isProp A := forall x y : A, x = y.
Module String_dec.
......@@ -271,9 +299,8 @@ Section subtyping.
Proof.
destruct B as [ | l B1 B2 ].
- exact true.
- case_eq (mem l (domain A)).
- case (Istrue_case (mem l (domain A))).
+ intro H.
apply Istrue_eq in H.
apply mem_pos in H.
case (type_dec (assoc A l H) B1); intro.
* exact (subtype_dec A B2).
......@@ -281,10 +308,25 @@ Section subtyping.
+ intro; exact false.
Defined.
Definition subtype_dec_correct A B : Istrue (subtype_dec A B) -> A <: B.
Fixpoint subtype_dec_correct A B : Istrue (subtype_dec A B) -> A <: B.
Proof.
admit.
Qed.
destruct B as [ | l B1 B2 ].
- simpl.
trivial.
- intro H.
simpl in H.
pose (Hi := Istrue_case_not_right _ _ H).
simpl in Hi.
pose (Hii := Istrue_case_not_right_fun _ _ H).
change (Istrue_case_not_right _ _ H) with Hi in Hii.
simpl in Hii.
exists (mem_pos l (domain A) Hi).
generalize Hii.
case (type_dec ((A l) (mem_pos l (domain A) Hi)) B1).
+ intros.
split; intuition.
+ intros _ H2; inversion H2.
Defined.
Fixpoint domain_subtype {A} {B} :
A <: B -> domain B domain A.
......@@ -366,7 +408,7 @@ Section objects.
*)
(* We have to axiomatize the type of methods because
Method A B := Obj A -> Obj B has a negative occurence of Obj which blocks
Method A B := Expr A -> Expr B has a negative occurence of Expr which blocks
the recursive definition
*)
......
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