Skip to content

Instantly share code, notes, and snippets.

@bkyrlach
Last active June 18, 2022 02:17
Show Gist options
  • Save bkyrlach/9295306b399a689eaad4f067e3e6f6fb to your computer and use it in GitHub Desktop.
Save bkyrlach/9295306b399a689eaad4f067e3e6f6fb to your computer and use it in GitHub Desktop.
Stuck on proofs...
Require Import String.
Inductive ty : Type :=
| TInt : ty
| TString : ty.
Inductive Value : Type :=
| VInt : nat -> Value
| VString : string -> Value.
Inductive Exp : Type :=
| ELit : Value -> Exp
| EVar : string -> Exp.
Inductive hasTy : (list (string * ty)) -> (Exp * ty) -> Prop :=
| ELit_int_ty : forall ctx n, hasTy ctx (ELit (VInt n), TInt)
| ELit_str_ty : forall ctx s, hasTy ctx (ELit (VString s), TString)
| EVar_ty : forall ctx name a,
(List.In (name, a) ctx) ->
hasTy ctx (EVar name, a).
Definition ty_eq (t1 t2 : ty) : { t1 = t2 } + {~ t1 = t2 }.
decide equality.
Defined.
Lemma pair_eq_dec : forall p1 p2: (string * ty), {p1 = p2} + {~ p1 = p2}.
Proof.
repeat decide equality.
Qed.
Lemma neq : forall p1 p2: (string * ty), (p1 = p2) -> (p1 <> p2) -> False.
Proof.
intros.
intuition.
Qed.
Lemma not_in : forall (ctx : list (string * ty)) (p : (string * ty)), (List.In p ctx) -> (~ List.In p ctx) -> False.
Proof.
intros.
intuition.
Qed.
Definition in_ctx (ctx : list (string * ty)) (p : (string * ty)) : { List.In p ctx } + {~ List.In p ctx}.
induction ctx.
right.
intros Hnot.
inversion Hnot.
destruct IHctx.
destruct (pair_eq_dec a p).
left.
simpl.
left.
apply e.
left.
simpl.
right.
apply i.
destruct (pair_eq_dec a p).
left.
simpl.
left.
apply e.
right.
simpl.
intros Hnot.
destruct Hnot.
apply (neq a p).
apply H.
apply n0.
apply (not_in ctx p).
apply H.
apply n.
Defined.
Definition is_int (ctx : list (string * ty)) (exp : Exp) : bool.
assert ((hasTy ctx (exp, TInt)) + (~ hasTy ctx (exp, TInt))).
induction exp.
induction v.
left.
apply (ELit_int_ty ctx n).
right.
intros Hnot.
inversion Hnot.
destruct (in_ctx ctx (s, TInt)).
left.
apply (EVar_ty ctx s TInt).
apply i.
right.
intros Hnot.
inversion Hnot.
apply (not_in ctx (s, TInt)).
apply H1.
apply n.
destruct H.
{
exact true.
}
{
exact false.
}
Defined.
Definition infer (ctx : list (string * ty)) (exp : Exp) : option (Exp * ty).
assert (is_int ctx exp).
@bkyrlach
Copy link
Author

New version. Don't understand what I'm doing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment