Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq: Add vec #272

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Coq: Add vec #272

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
135 changes: 127 additions & 8 deletions coq/MiniCandid.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,11 @@ MiniCandid: A formalization of the core ideas of Candid

Require Import FunInd.

Require Import Psatz.

Require Import Coq.ZArith.BinInt.
Require Import Coq.Init.Datatypes.
Require Import Coq.Lists.List.

Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Relations.Relation_Definitions.
Expand All @@ -24,6 +27,7 @@ CoInductive T :=
| IntT: T
| NullT : T
| OptT : T -> T
| VecT : T -> T
| VoidT : T
| ReservedT : T
.
Expand All @@ -33,6 +37,7 @@ Inductive V :=
| IntV : Z -> V
| NullV : V
| SomeV : V -> V
| VecV : list V -> V
| ReservedV : V
.

Expand Down Expand Up @@ -71,6 +76,9 @@ Inductive HasType : V -> T -> Prop :=
| OptHT:
case optHT,
forall v t, v :: t -> SomeV v :: OptT t
| VecHT:
case vecHT,
forall vs t, (forall n, n < length vs -> nth n vs NullV :: t) -> VecV vs :: VecT t
| ReservedHT:
case reservedHT,
ReservedV :: ReservedT
Expand All @@ -87,10 +95,10 @@ Here things are simple and inductive.
Reserved Infix "<:" (at level 80, no associativity).
CoInductive Subtype : T -> T -> Prop :=
| ReflST :
case reflSL,
case reflST,
forall t, t <: t
| NatIntST :
case natIntSL,
case natIntST,
NatT <: IntT
| NullOptST :
case nullOptST,
Expand All @@ -107,6 +115,11 @@ CoInductive Subtype : T -> T -> Prop :=
forall t1 t2,
is_opt_like_type t2 = false ->
t1 <: t2 -> t1 <: OptT t2
| VecST :
case vecST,
forall t1 t2,
t1 <: t2 ->
VecT t1 <: VecT t2
| VoidST :
case voidST,
forall t, VoidT <: t
Expand Down Expand Up @@ -144,6 +157,12 @@ Inductive Coerces : V -> V -> T -> Prop :=
is_not_opt_like_value v1 ->
v1 ~> v2 :: t ->
v1 ~> SomeV v2 :: OptT t
| VecC:
case vecC,
forall vs1 vs2 t,
length vs1 = length vs2 ->
(forall n, n < length vs1 -> nth n vs1 NullV ~> nth n vs2 NullV :: t) ->
VecV vs1 ~> VecV vs2 :: VecT t
| ReservedC:
case reservedC,
forall v1,
Expand All @@ -162,13 +181,36 @@ Qed.
Theorem coercion_correctness:
forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
Proof.
intros. induction H; constructor; assumption.
intros. induction H; try (named_constructor; assumption); name_cases.
[vecC]: {
named_constructor.
intros.
apply H1. lia.
}
Qed.

Theorem coercion_roundtrip:
forall v t, v :: t -> v ~> v :: t.
Proof.
intros. induction H; constructor; intuition.
intros. induction H; try (constructor; intuition); name_cases.
Qed.

Lemma nths_ext:
forall A (l1 l2 : list A) d,
length l1 = length l2 ->
(forall n, n < length l1 -> nth n l1 d = nth n l2 d) ->
l1 = l2.
Proof.
intros A l1. induction l1; intros l2 d Heq Hnth.
* destruct l2; inversion Heq. reflexivity.
* destruct l2; inversion Heq.
f_equal.
- specialize (Hnth 0 ltac:(simpl;lia)).
simpl in Hnth. assumption.
- eapply IHl1; try assumption.
intros n Hle.
specialize (Hnth (S n) ltac:(simpl;lia)).
simpl in Hnth. eassumption.
Qed.

Theorem coercion_uniqueness:
Expand All @@ -177,7 +219,16 @@ Proof.
intros.
revert v2 H0.
induction H; intros v2' Hother;
try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence).
try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence);
name_cases.
[vecC]: {
inversion Hother; subst; clear Hother.
apply f_equal.
eapply nths_ext; try congruence.
intros n Hle.
apply H1; try congruence.
apply H6; congruence.
}
Qed.

Theorem soundness_of_subtyping:
Expand All @@ -196,9 +247,9 @@ Proof.
}
[intHT_constituentOptST]: {
inversion H0; subst; clear H0; simpl in H; inversion H.
econstructor. named_econstructor; [constructor|named_constructor].
eexists. named_econstructor; [constructor|named_constructor].
}
[optHT_reflSL]: {
[optHT_reflST]: {
specialize (IHHvT t (ReflST _ _)).
destruct IHHvT as [v2 Hv2].
eexists. named_econstructor; try eassumption.
Expand All @@ -211,6 +262,64 @@ Proof.
[optHT_constituentOptST]: {
inversion H0; subst; clear H0; simpl in H; inversion H.
}
[vecHT_vecST]: {
clear H.
assert (Hv2 : forall n : nat, n < length vs -> exists v2 : V, nth n vs NullV ~> v2 :: t2) by intuition.
clear H0 H2.
induction vs.
* exists (VecV nil). named_constructor; try reflexivity. intuition. simpl in H. lia.
* lapply IHvs.
- intros. destruct H as [v2 HC].
inversion HC; subst; clear HC.
destruct (Hv2 0 ltac:(simpl;lia)) as [va HCa].
exists (VecV (va :: vs2)).
named_constructor.
+ simpl; congruence.
+ intros. simpl in H.
destruct n.
** apply HCa.
** apply H3. lia.
- intros.
specialize (Hv2 (S n) ltac:(simpl;lia)).
firstorder.
}
[vecHT_reflST]: {
eexists. named_constructor.
* reflexivity.
* intros.
apply coercion_roundtrip.
apply H.
assumption.
}
[vecHT_constituentOptST]: {
inversion H2; subst; clear H2; simpl in H1; inversion H1.
* eexists.
named_constructor; try reflexivity.
named_constructor; try reflexivity.
intros. apply coercion_roundtrip. apply H. assumption.
* enough (exists v2 : V, VecV vs ~> v2 :: VecT t0)
by (destruct H2; eexists; named_constructor; try reflexivity; apply H2).
assert (Hv2 : forall n : nat, n < length vs -> exists v2 : V, nth n vs NullV ~> v2 :: t0) by intuition.
clear H H0 H1 vecST H4 t.
{
induction vs.
* exists (VecV nil). named_constructor; try reflexivity. intuition. simpl in H. lia.
* lapply IHvs.
- intros. destruct H as [v2 HC].
inversion HC; subst; clear HC.
destruct (Hv2 0 ltac:(simpl;lia)) as [va HCa].
exists (VecV (va :: vs2)).
named_constructor.
+ simpl; congruence.
+ intros. simpl in H.
destruct n.
** apply HCa.
** apply H3. lia.
- intros.
specialize (Hv2 (S n) ltac:(simpl;lia)).
firstorder.
}
}
[reservedHT_constituentOptST]: {
inversion H0; subst; clear H0; simpl in H; inversion H.
}
Expand All @@ -232,7 +341,7 @@ Proof.
inversion H2; subst; clear H2;
name_cases;
try (constructor; easy).
[natIntSL_constituentOptST]: {
[natIntST_constituentOptST]: {
named_constructor.
- assumption.
- eapply Hyp; [named_econstructor | assumption].
Expand All @@ -256,6 +365,16 @@ Proof.
[reservedST_constituentOptST]: {
inversion H0; subst; clear H0; inversion H.
}
[vecST_vecST0]: {
named_constructor.
eapply Hyp; eassumption.
}
[vecST_constituentOptST]: {
named_constructor; try assumption.
inversion H1; subst; clear H1; try easy.
- named_constructor; assumption.
- named_constructor. eapply Hyp; eassumption.
}
Qed.

End NoOpportunisticDecoding.
Expand Down