Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

corrected LibTactics.v; finished UseTactics.v

  • Loading branch information...
commit 9ae25f9242c1c8725f9d88100cb12d441778daca 1 parent b7f96f9
@timjb authored
Showing with 12 additions and 8 deletions.
  1. +1 −1  LibTactics.v
  2. +11 −7 UseTactics.v
View
2  LibTactics.v
@@ -404,7 +404,7 @@ Ltac fast_rm_inside E :=
In order for tactics to convert their arguments into natural numbers,
we provide a conversion tactic. *)
-Require Coq.NArith.BinPos Coq.ZArith.BinInt.
+Require Coq.PArith.BinPos Coq.ZArith.BinInt.
Definition ltac_nat_from_int (x:BinInt.Z) : nat :=
match x with
View
18 UseTactics.v
@@ -96,7 +96,7 @@ Admitted.
Theorem exists_impl: forall X (P : X -> Prop) (Q : Prop) (R : Prop),
(forall x, P x -> Q) ->
- ((exists x : X, P x) -> Q).
+ ((exists (x : X), P x) -> Q).
Proof.
introv [x H2]. eauto.
(* same as [intros X P Q R H1 [x H2].], which is itself short
@@ -1048,8 +1048,7 @@ Proof with eauto.
(* old: destruct (typing_inversion_var _ _ _ Htypt) as [T [Hctx Hsub]].*)
(* new: *) lets (T&Hctx&Hsub): typing_inversion_var Htypt.
unfold extend in Hctx.
- remember (beq_id x y) as e. destruct e...
- (* Note: [cases_if'] could be used to simplify the line above *)
+ cases_if' as Heqe...
SCase "x=y".
apply beq_id_eq in Heqe. subst.
inversion Hctx; subst. clear Hctx.
@@ -1067,8 +1066,9 @@ Proof with eauto.
(* Exercise: replace the following [destruct] with a [lets]. *)
(* old: destruct (typing_inversion_app _ _ _ _ Htypt)
as [T1 [Htypt1 Htypt2]]. eapply T_App... *)
- (* FILL IN HERE *) admit.
-
+ lets (T1 & Htypt1 & Htypt2): typing_inversion_app Htypt.
+ eapply T_App...
+
Case "tabs".
rename i into y. rename t into T1.
@@ -1103,8 +1103,12 @@ Proof with eauto.
(* old: assert (subtype TUnit S)
by apply (typing_inversion_unit _ _ Htypt)... *)
(* new: *) lets: typing_inversion_unit Htypt...
-
-
+ Case "tpair".
+ lets (T1&T2&Htyp1&Htyp2&H): typing_inversion_pair Htypt...
+ Case "tfst".
+ lets (T1&T2&Htyp&H): typing_inversion_fst Htypt...
+ Case "tsnd".
+ lets (T1&T2&Htyp&H): typing_inversion_snd Htypt...
Qed.
End ExamplesInstantiations.
Please sign in to comment.
Something went wrong with that request. Please try again.