Commit 36e97ba3 authored by Michael Sammler's avatar Michael Sammler Committed by Paul
Browse files

fix newly added admitteds

parent 0b13dc15
......@@ -97,7 +97,13 @@ Fixpoint check_has_ty_conditions (t : tm) (r : option range) : list Prop :=
Lemma check_has_ty_mv_conditions t σ:
check_has_ty t (mv σ) = true Forall id (check_has_ty_conditions t None).
Proof. Admitted.
Proof.
induction t => //=.
all: try case_match => //=.
all: try match goal with | |- context [ (?o = _) ] => destruct o eqn:Heqn end => //=.
all: rewrite ?andb_true_iff ?Forall_app.
all: naive_solver.
Qed.
Lemma check_has_ty_spec t τ :
Forall id (check_has_ty_conditions t (if τ is val σ f then Some (sig_ranges σ !!! f) else None))
......@@ -140,5 +146,9 @@ Lemma has_ty_implies_check_has_ty_conditions t τ :
Proof.
revert τ. induction t => τ; destruct τ; try case_match.
all: simpl => //; inversion 1; simplify_option_eq.
all: try match goal with | H : recognize _ _ = Some _ |- _ => move: (H) => /recognize_spec?; subst end.
all: try have ? := IHt _ ltac:(eassumption).
all: try have ? := IHt1 _ ltac:(eassumption).
all: try have ? := IHt2 _ ltac:(eassumption).
all: rewrite ?Forall_app; eauto.
Admitted.
Qed.
Supports Markdown
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