Skip to content

Instantly share code, notes, and snippets.

@JasonGross
Created August 19, 2014 21:52
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save JasonGross/642b62458ace7e98eee3 to your computer and use it in GitHub Desktop.
Diff to get outrageous to work with Coq trunk (output of svn diff)
Index: TreeItrp.v
===================================================================
--- TreeItrp.v (revision 16)
+++ TreeItrp.v (working copy)
@@ -1,3 +1,4 @@
+Set Asymmetric Patterns.
Require Import List.
Require Import Utils.
Index: Context.v
===================================================================
--- Context.v (revision 16)
+++ Context.v (working copy)
@@ -1,3 +1,4 @@
+Set Asymmetric Patterns.
Require Import Utils.
Require Import SimpSubst.
@@ -121,7 +122,7 @@
: forall G (s:CtxS G) n T (a:AtCtx (ctx s) n T),P _ _ _ a.
refine (fix atCtxIndS G s n := match s in CtxS G return forall T (a:AtCtx (ctx s) n T),P _ _ _ a with
empCtxS => _ |
- extCtxS _ s _ => _
+ extCtxS G0 s0 _ => _
end);clear G s;simpl;intro.
intro.
@@ -157,7 +158,7 @@
change (PopCtx T' (AtCtx G n) T2) in a2.
destruct a2 as (T2,a2).
- exact (tr (fun xa=>_ = exAtCtx (popCtx (xa_a xa) T')) (IHa1 _ a2) (eq_refl _)).
+ exact (tr (fun xa=>exAtCtx (popCtx a1 T') = exAtCtx (popCtx (xa_a xa) T')) (IHa1 _ a2) (eq_refl _)).
Defined.
Implicit Arguments atCtxUniq [G n T1 T2].
@@ -222,8 +223,8 @@
Definition extSCtxInv GL n G T (xg:ExtCtx GL (S n) (extCtx G T)) (P:forall n G T,ExtCtx GL n (extCtx G T)->Type)
(xgS:forall xg:ExtCtx GL n G,P _ _ _ (extSCtx xg T))
: P _ _ _ xg.
- pose (P' n Gx (xg:ExtCtx GL n Gx) := forall ne:IsExtCtx Gx,
- P _ _ _ (tr (ExtCtx GL n) (extCtxUnfold ne) xg)).
+ pose (P' n0 Gx (xg:ExtCtx GL n0 Gx) := forall ne:IsExtCtx Gx,
+ P _ _ _ (tr (ExtCtx GL n0) (extCtxUnfold ne) xg)).
assert (Peq := match G as G return forall T xg,P (S n) G T xg = P _ (ctx (ctxSc G)) _ xg
with ctx _ _ => fun _ _=>eq_refl _ end T).
apply (tr (fun C=>C) (eq_sym (Peq _))).
@@ -233,7 +234,7 @@
extSCtx _ _ xg0 _ => fun Hn HG=>_
end (eq_refl _) (eq_refl _)).
revert xg0.
- apply (tr (fun _=>_) (eq_sym (Sinj Hn))).
+ apply Sinj in Hn; subst.
apply (tr (fun GT=>forall xg,P' _ _ (extSCtx xg (projT2 GT))) (extCtxInj HG)).
simpl.
intros ? ?.
@@ -379,7 +380,9 @@
change (elBump P (extSCtx xg T') (ctxProj (popCtx a T')) =
ctxProj (popCtx (atBumpLo P xg a Ho) (elBump P xg T'))).
apply (tr (fun X=>_ = X) (ctxProj_pop (atBumpLo P xg a Ho) (elBump P xg T'))).
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHa _ Ho xg)).
+ specialize (IHa _ Ho xg).
+ let XT := match type of IHa with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHa).
reflexivity.
Defined.
Implicit Arguments ctxProj_BumpLo [GL l G n T].
@@ -407,7 +410,9 @@
ctxProj (popCtx (atBumpHi P xg a Ho) (elBump P xg T'))).
apply (tr (fun X=>elBump P (extSCtx xg T') X = _) (ctxProj_pop a T')).
apply (tr (fun X=>_ = X) (ctxProj_pop (atBumpHi P xg a Ho) (elBump P xg T'))).
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHxg _ Ho _ a)).
+ specialize (IHxg _ Ho _ a).
+ let XT := match type of IHxg with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X:XT=>_ = fun g=>X (projT1 g)) IHxg).
reflexivity.
Defined.
Implicit Arguments ctxProj_BumpHi [GL l G n T].
@@ -519,7 +524,9 @@
change (PopCtx T (AtCtx G a) P') in a'.
destruct a' as (P',a').
- apply (tr (fun _=>_) (IHxg _ a')).
+ specialize (IHxg _ a').
+ let XT := match type of IHxg with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHxg).
reflexivity.
Defined.
Implicit Arguments atMBumpTEq [GL a b P G P'].
@@ -576,7 +583,9 @@
change (elSubst (extSCtx xg T') (ctxProj (popCtx a T')) p =
ctxProj (popCtx (atSubstLt xg a Ho p) (elSubst xg T' p))).
apply (tr (fun X=>_ = X) (ctxProj_pop (atSubstLt xg a Ho p) (elSubst xg T' p))).
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHa _ Ho xg)).
+ specialize (IHa _ Ho xg).
+ let XT := match type of IHa with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHa).
reflexivity.
Defined.
Implicit Arguments ctxProj_SubstLt [GL P l G n T].
@@ -605,8 +614,10 @@
ctxProj (popCtx (atSubstGt xg a Ho p) (elSubst xg T' p))).
apply (tr (fun X=>elSubst (extSCtx xg T') X p = _) (ctxProj_pop a T')).
apply (tr (fun X=>_ = X) (ctxProj_pop (atSubstGt xg a Ho p) (elSubst xg T' p))).
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHxg _ Ho _ a)).
- reflexivity.
+ specialize (IHxg _ Ho _ a).
+ let XT := match type of IHxg with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHxg).
+ reflexivity.
Defined.
Implicit Arguments ctxProj_SubstGt [GL P l G n T].
@@ -637,7 +648,8 @@
simpl ctxTp.
intros ? ? a' ? ?.
simpl elMBump.
- apply (tr (fun t=>_ = fun g=>t (projT1 g)) H).
+ let XT := match type of H with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) H).
simpl atMBumpTEq.
refine (match atMBumpTEq b' xg a' as teq
return ctxProj (tr (AtCtx (extCtx (ctx s) _) _) (tr _ teq _) _) =
@@ -661,7 +673,8 @@
intros.
change ((fun g:ctxSubst (extSCtx xg T) p=>elSubst xg (ctxProj a) p (projT1 g)) =
(fun g=>elSubst xg (elMBump xg a p) p (projT1 g))).
- apply (tr (fun X=>_ = fun g:ctxSubst (extSCtx xg T) p=>X (projT1 g)) H).
+ let XT := match type of H with _ = _ :> ?XT => constr:(XT) end in
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) H).
reflexivity.
Defined.
Implicit Arguments ctxProj_SubstEq [GL P n G P'].
Index: TreeSyntax.v
===================================================================
--- TreeSyntax.v (revision 16)
+++ TreeSyntax.v (working copy)
@@ -1,3 +1,4 @@
+Set Asymmetric Patterns.
Require Import List.
Require Import Compare_dec.
@@ -478,7 +479,7 @@
replace n0 with (length (firstn n G));subst n0.
apply tfGoodBump_O with (1 := H0).
rewrite firstn_length.
- apply MinMax.min_l with (1 := H).
+ apply min_l with (1 := H).
Qed.
Lemma tfGoodSubstNest GL GR F b : (b < length GL)->let X := fBump (S b) O (nth b GL Uv) in
@@ -872,8 +873,8 @@
apply ctxProjGood with (1 := H0).
simpl in H3.
rewrite <- H2.
- exact H3.
+ assumption.
refine (let H := IHSimpFamOK _ in _).
apply tcGoodCons with (1 := H1) (2 := H0).
- apply tfGoodPi with (1 := H1) (2 := H2).
+ apply tfGoodPi; assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment