logrel.v 21 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import F_mu_ref.lang F_mu_ref.typing F_mu_ref.rules.
From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Import uPred.

(** interp : is a unary logical relation. *)
Section logrel.
  Context {Σ : gFunctors}.
  Notation "# v" := (of_val v) (at level 20).

  Canonical Structure leibniz_val := leibnizC val.

18
  Canonical Structure leibniz_var := leibnizC var.
19

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
  Class Val_to_IProp_Persistent (f : leibniz_val -n> iPropG lang Σ) :=
    val_to_iprop_persistent :  v : val, PersistentP ((cofe_mor_car _ _ f) v).

  Arguments Val_to_IProp_Persistent /.

  (** Just to get nicer closed forms, we define extend_context_interp in three steps. *)
  Program Definition extend_context_interp_fun1
    (τi : leibniz_val -n> iPropG lang Σ)
    (f : leibniz_var -n> leibniz_val -n> iPropG lang Σ) :
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) :=
    {| cofe_mor_car :=
         λ x,
         match x return leibniz_val -n> iPropG lang Σ with
         | O => τi
         | S x' => f x'
         end
36
37
    |}.

38
39
40
41
  Program Definition extend_context_interp_fun2
    (τi : leibniz_val -n> iPropG lang Σ) :
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) :=
42
    {|
43
      cofe_mor_car := λ f, extend_context_interp_fun1 τi f
44
    |}.
45
46
  Next Obligation.
  Proof. intros ???? Hfg x; destruct x; cbn; trivial. Qed.
47

48
49
50
51
  Program Definition extend_context_interp :
    (leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) :=
52
    {|
53
      cofe_mor_car := λ τi, extend_context_interp_fun2 τi
54
    |}.
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
  Next Obligation.
  Proof. intros n g h H Δ x y. destruct x; cbn; auto. Qed.

  Program Definition extend_context_interp_apply :
    ((leibniz_var -n> leibniz_val -n> iPropG lang Σ)) -n>
    ((leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n>
     leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ) :=
    {|
      cofe_mor_car := λ Δ,
        {|
          cofe_mor_car := λ f,
            {|
              cofe_mor_car := λ g, f (extend_context_interp g Δ)
            |}
        |}
    |}.
  Solve Obligations with
  repeat intros ?; (cbn + idtac);
    try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.
  Next Obligation.
76
  Proof.
77
78
79
80
81
82
83
    intros n Δ Δ' HΔ f g x.  cbn.
    match goal with
      |- _ _ ?F x {n} _ _ ?G x =>
      assert (F {n} G) as HFG; [|rewrite HFG; trivial]
    end.
    apply cofe_mor_car_ne; trivial. intros y. cbn.
    destruct y; trivial.
84
85
  Qed.

86
  Definition interp_unit : leibniz_val -n> iPropG lang Σ :=
87
    {|
88
      cofe_mor_car := λ w, (w = UnitV)%I
89
90
    |}.

91
92
93
  Program Definition interp_prod :
    (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ) -n>
    leibniz_val -n> iPropG lang Σ :=
94
95
    {|
      cofe_mor_car :=
96
97
98
99
100
101
102
103
104
        λ τ1i,
        {|
          cofe_mor_car :=
            λ τ2i,
            {|
              cofe_mor_car :=
                λ w, ( w1 w2, w = PairV w1 w2   τ1i w1   τ2i w2)%I
            |}
        |}
105
    |}.
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
  Solve Obligations with
  repeat intros ?; cbn;
    repeat apply exist_ne =>?;
        try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.

  Program Definition interp_sum :
    (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ) -n>
    leibniz_val -n> iPropG lang Σ :=
    {|
      cofe_mor_car :=
        λ τ1i,
        {|
          cofe_mor_car :=
            λ τ2i,
            {|
              cofe_mor_car :=
                λ w, (( w1, w = InjLV w1   τ1i w1) 
                      ( w2, w = InjRV w2   τ2i w2))%I
            |}
        |}
    |}.
  Solve Obligations with
  repeat intros ?; cbn; try apply or_ne;
    try apply exist_ne =>?;
        try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.

  Program Definition interp_arrow :
    (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ) -n>
    leibniz_val -n> iPropG lang Σ :=
    {|
      cofe_mor_car :=
        λ τ1i,
        {|
          cofe_mor_car :=
            λ τ2i,
            {|
              cofe_mor_car :=
                λ w, (  v,  τ1i v  WP (App (# w) (# v)) @  {{τ2i}})%I
            |}
        |}
    |}.
  Solve Obligations with
  repeat intros ?; cbn;
    try apply always_ne;
    try apply forall_ne=>?; try apply impl_ne; trivial;
      try apply wp_ne =>?;
          try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.

  Program Definition interp_forall :
    ((leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ)) -n>
    leibniz_val -n> iPropG lang Σ :=
    {|
      cofe_mor_car :=
        λ τi,
        {|
          cofe_mor_car :=
            λ w,
            ( e, w = TLamV e 
                   (τ'i : {f : (leibniz_val -n> iPropG lang Σ) |
                            Val_to_IProp_Persistent f}),
                     ( WP e @  {{λ v, (τi (`τ'i) v)}}))%I
        |}
    |}.
  Next Obligation.
170
  Proof.
171
172
    intros τ τ' x y Hxy; cbn. apply exist_ne => e; apply and_ne; auto.
    rewrite Hxy; trivial.
173
  Qed.
174
175
176
177
178
  Next Obligation.
    intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
    apply forall_ne=> P.
    apply always_ne, (contractive_ne _), wp_ne => w.
    rewrite Hfg; trivial.
179
180
  Qed.

181
182
183
184
  Program Definition interp_rec_pre :
    ((leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ)) -n>
    (leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_val -n> iPropG lang Σ) :=
185
    {|
186
187
188
189
190
191
192
193
      cofe_mor_car :=
        λ τi,
        {| cofe_mor_car :=
             λ rec_appr,
             {|
               cofe_mor_car := λ w, ( ( v, w = FoldV v   (τi rec_appr v)))%I
             |}
        |}
194
    |}.
195
196
197
198
199
  Next Obligation.
  Proof.
    intros τi rec_appr n x y Hxy; rewrite Hxy; trivial.
  Qed.
  Next Obligation.
200
  Proof.
201
202
    intros τi n f g Hfg x. cbn.
    apply always_ne, exist_ne =>w; rewrite Hfg; trivial.
203
  Qed.
204
  Next Obligation.
205
  Proof.
206
207
    intros n τi τi' Hτi f x. cbn.
    apply always_ne, exist_ne =>w; rewrite Hτi; trivial.
208
  Qed.
209

210
  Global Instance interp_rec_pre_contr
211
         (τi : (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ))
212
213
214
215
    :
      Contractive (interp_rec_pre τi).
  Proof.
    intros n f g H w; cbn.
216
    apply always_ne, exist_ne; intros e; apply and_ne; trivial.
217
    apply later_contractive =>i Hi.
218
    rewrite H; trivial.
219
220
  Qed.

221
222
223
224
225
226
227
228
229
  Program Definition interp_rec :
    ((leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ)) -n>
    (leibniz_val -n> iPropG lang Σ)
    :=
      {|
        cofe_mor_car := λ τi, fixpoint (interp_rec_pre τi)
      |}.
  Next Obligation.
  Proof. intros n f g H; apply fixpoint_ne => z; rewrite H; trivial. Qed.
230
231
232
233

  Context `{i : heapG Σ}.
  Context `{L : namespace}.

234
235
236
237
238
239
240
  Program Definition interp_ref_pred (l : loc) :
    (leibniz_val -n> iPropG lang Σ) -n> iPropG lang Σ :=
    {|
      cofe_mor_car := λ τi, ( v, l  v  (τi v))%I
    |}.
  Next Obligation.
  Proof. intros ???? H; apply exist_ne =>w; rewrite H; trivial. Qed.
241

242
243
  Program Definition interp_ref :
    (leibniz_val -n> iPropG lang Σ) -n> leibniz_val -n> iPropG lang Σ :=
244
245
    {|
      cofe_mor_car :=
246
247
248
249
        λ τi, {|
          cofe_mor_car :=
            λ w, ( l, w = LocV l  inv (L .@ l) (interp_ref_pred l τi))%I
        |}
250
    |}.
251
252
253
  Next Obligation.
  Proof. intros ???? H; rewrite H; trivial. Qed.
  Next Obligation.
254
  Proof.
255
256
    intros ??? H ?; apply exist_ne=>w; apply and_ne; trivial; cbn.
    apply (contractive_ne _); apply exist_ne=>w'; rewrite H; trivial.
257
258
  Qed.

259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
  Program Fixpoint interp (τ : type) {struct τ}
    : (leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n> leibniz_val -n> iPropG lang Σ
    :=
      match τ return (leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n>
                     leibniz_val -n> iPropG lang Σ
      with
      | TUnit => {| cofe_mor_car := λ Δ, interp_unit |}
      | TProd τ1 τ2 => {| cofe_mor_car := λ Δ, interp_prod (interp τ1 Δ) (interp τ2 Δ)|}
      | TSum τ1 τ2 => {| cofe_mor_car := λ Δ, interp_sum(interp τ1 Δ) (interp τ2 Δ)|}
      | TArrow τ1 τ2 => {|cofe_mor_car := λ Δ, interp_arrow (interp τ1 Δ) (interp τ2 Δ)|}
      | TVar v => {| cofe_mor_car :=
                      λ Δ : (leibniz_var -n> (leibniz_val -n> iPropG lang Σ)), (Δ v)  |}
      | TForall τ' =>
        {| cofe_mor_car :=
             λ Δ, interp_forall  (extend_context_interp_apply Δ (interp τ')) |}
      | TRec τ' =>
        {| cofe_mor_car :=
             λ Δ, interp_rec
                    (extend_context_interp_apply Δ (interp τ')) |}
      | Tref τ' => {| cofe_mor_car := λ Δ, interp_ref (interp τ' Δ) |}
      end%I.
  Solve Obligations
  with repeat intros ?; match goal with [H : _ {_} _|- _] => rewrite H end; trivial.

  Class context_interp_Persistent (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ) :=
    contextinterppersistent :  v : var, Val_to_IProp_Persistent (Δ v).

  Global Instance Val_to_IProp_Persistent_Persistent
         (f : leibniz_val -n> iPropG lang Σ)
         {Hf : Val_to_IProp_Persistent f}
         (v : val)
290
    : PersistentP (f v).
291
  Proof. apply Hf. Qed.
292
293
294
295
296

  Global Instance interp_Persistent
         τ (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
         {HΔ : context_interp_Persistent Δ}
    : Val_to_IProp_Persistent (interp τ Δ).
297
  Proof.
298
299
300
301
302
    revert Δ HΔ.
    induction τ; cbn; intros Δ HΔ v; try apply _.
    - rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
      apply always_intro'; trivial.
    - apply Val_to_IProp_Persistent_Persistent; apply HΔ.
303
304
  Qed.

305
306
307
  Global Instance Persistent_context_interp_rel Δ Γ vs
           {HΔ : context_interp_Persistent Δ}
    : PersistentP (Π∧ zip_with(λ τ v, interp τ Δ v) Γ vs)%I.
308
309
  Proof. typeclasses eauto. Qed.

310
311
312
313
314
315
316
  Global Program Instance extend_context_interp_Persistent f Δ
           (Hf : Val_to_IProp_Persistent f)
           {HΔ : context_interp_Persistent Δ}
    : context_interp_Persistent (@extend_context_interp f Δ).
  Next Obligation.
    intros f Δ Hf HΔ v w; destruct v; cbn; trivial.
    apply HΔ.
317
318
  Qed.

319
  Local Ltac properness :=
320
321
    repeat
      match goal with
322
323
324
325
326
327
328
329
330
331
      | |- ( _: _, _)%I  ( _: _, _)%I => apply exist_proper =>?
      | |- ( _: _, _)%I  ( _: _, _)%I => apply forall_proper =>?
      | |- (_  _)%I  (_  _)%I => apply and_proper
      | |- (_  _)%I  (_  _)%I => apply or_proper
      | |- (_  _)%I  (_  _)%I => apply impl_proper
      | |- (WP _ {{ _ }})%I  (WP _ {{ _ }})%I => apply wp_proper =>?
      | |- ( _)%I  ( _)%I => apply later_proper
      | |- ( _)%I  ( _)%I => apply always_proper
      | |- (inv _ _)%I  (inv _ _)%I => apply (contractive_proper _)
      | |- (_  _)%I  (_  _)%I => apply sep_proper
332
333
      end.

334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
  Lemma interp_unused_contex_irrel
        (m n : nat)
        (Δ Δ' : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
        (HΔ :  v, Δ (if lt_dec v m then v else (n + v)) 
                     Δ' (if lt_dec v m then v else (n + v)))
        (τ : type)
    :
      interp τ.[iter m up (ren (+n))] Δ  interp τ.[iter m up (ren (+n))] Δ'.
  Proof.
    revert m n Δ Δ' HΔ.
    induction τ; intros m n Δ Δ' HΔ v; cbn; auto.
    - properness; trivial; try apply IHτ1; try apply IHτ2; trivial.
    - properness; trivial; try apply IHτ1; try apply IHτ2; trivial.
    - properness; trivial; try apply IHτ1; try apply IHτ2; trivial.
    - match goal with
        |- _ _ ?f ?x  _ _ ?g ?x =>
        assert (f  g) as Hfg; [|rewrite Hfg; trivial]
      end.
      apply fixpoint_proper => ??; cbn.
      properness; trivial.
      change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
      apply IHτ.
      {
        intros x y. destruct x; cbn; trivial.
        destruct lt_dec.
        - specialize (HΔ x); destruct lt_dec; auto with omega.
        - destruct (n + S x) as [|k] eqn:Heq; trivial.
          specialize (HΔ x); destruct lt_dec; auto with omega.
          replace (n + x) with k in HΔ by omega; trivial.
      }
    -  rewrite iter_up. destruct lt_dec; cbn.
       + specialize (HΔ x); destruct lt_dec; auto with omega.
       + asimpl; unfold ids; cbn.
         specialize (HΔ x); destruct lt_dec; auto with omega.
         replace (m + n + (x - m)) with (n + x) by omega. trivial.
    - properness; trivial.
      change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
      apply IHτ.
      {
        intros x y. destruct x; cbn; trivial.
        destruct lt_dec.
        - specialize (HΔ x); destruct lt_dec; auto with omega.
        - destruct (n + S x) as [|k] eqn:Heq; trivial.
          specialize (HΔ x); destruct lt_dec; auto with omega.
          replace (n + x) with k in HΔ by omega; trivial.
      }
    - properness; trivial; try apply IHτ; trivial.
  Qed.
382

383
384
385
386
387
388
389
390
391
392
393
394
395
  Program Definition hop_context_interp (m n : nat) :
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) :=
    {| cofe_mor_car :=
         λ Δ,
         {| cofe_mor_car := λ v, if lt_dec v m then Δ v else Δ (v - n) |}
    |}.
  Next Obligation.
  Proof. intros ?????? Hxy; destruct Hxy; trivial. Qed.
  Next Obligation.
  Proof.
    intros ????? Hfg ?; cbn. destruct lt_dec; rewrite Hfg; trivial.
  Qed.
396

397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
  Lemma extend_bofore_hop_context_interp (m n : nat)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
        (τi : leibniz_val -n> iPropG lang Σ)
        (v : var)
    :
      (extend_context_interp τi (hop_context_interp m n Δ)
                             (if lt_dec v (S m) then v else n + v))
         (hop_context_interp (S m) n (extend_context_interp τi Δ)
                              (if lt_dec v (S m) then v else n + v)).
  Proof.
    destruct v; cbn; trivial.
    repeat (destruct lt_dec; cbn); auto with omega.
    destruct (n + S v - n) eqn:Heq1;
      destruct (n + S v) eqn:Heq2; try destruct lt_dec; auto with omega.
    match goal with
      [ |- _ _ _ Δ ?a  _ _ _ Δ ?b] => assert (Heq : a = b) by omega; rewrite Heq; trivial
    end.
  Qed.
415
416

  Lemma interp_subst_weaken
417
418
        (m n : nat)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
419
        (τ : type)
420
    : interp τ Δ  interp τ.[iter m up (ren (+n))] (hop_context_interp m n Δ).
421
  Proof.
422
423
424
425
426
427
428
429
430
431
432
433
    revert m n Δ.
    induction τ; intros m n Δ v; cbn -[extend_context_interp]; auto.
    - properness; trivial; try apply IHτ1; try apply IHτ2.
    - properness; trivial; try apply IHτ1; try apply IHτ2.
    - properness; trivial; try apply IHτ1; try apply IHτ2.
    - match goal with
        |- _ _ ?f ?x  _ _ ?g ?x =>
        assert (f  g) as Hfg; [|rewrite Hfg; trivial]
      end.
      apply fixpoint_proper => ??; cbn -[extend_context_interp].
      properness; trivial.
      rewrite IHτ.
434
      change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
435
436
437
438
439
440
441
442
443
444
445
446
447
      apply interp_unused_contex_irrel.
      intros w; rewrite extend_bofore_hop_context_interp; trivial.
    - rewrite iter_up.
      asimpl; unfold ids; cbn; destruct lt_dec; cbn; destruct lt_dec; auto with omega.
      replace (m + n + (x - m)) with (x + n) by omega.
      replace (x + n - n) with x; trivial.
      { (** An incompleteness in omega and lia! *)
        clear.
        replace (x + n) with (n + x) by omega.
        induction n; cbn; auto with omega.
        induction x; cbn; trivial.
      }
    - properness; trivial.
448
      change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
449
450
451
452
      rewrite IHτ.
      apply interp_unused_contex_irrel.
      intros w; rewrite extend_bofore_hop_context_interp; trivial.
    - properness; trivial; try apply IHτ; trivial.
453
454
  Qed.

455
456
  Lemma interp_ren_S (τ : type)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
457
        (τi : leibniz_val -n> iPropG lang Σ)
458
    : interp τ Δ  interp τ.[ren (+1)] (extend_context_interp τi Δ).
459
  Proof.
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
    rewrite (interp_subst_weaken 0 1).
    apply interp_unused_contex_irrel.
    { clear. intros [|v]; cbn; trivial. }
  Qed.

  Local Opaque eq_nat_dec.

  Program Definition context_interp_insert (m : nat) :
    (leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) -n>
    (leibniz_var -n> leibniz_val -n> iPropG lang Σ) :=
    {| cofe_mor_car :=
         λ τi,
         {| cofe_mor_car :=
              λ Δ,
              {| cofe_mor_car :=
                   λ v, if lt_dec v m then Δ v else
                          if eq_nat_dec v m then τi else Δ (v - 1)
              |}
         |}
    |}.
  Next Obligation.
  Proof. intros m τi Δ n x y Hxy; destruct Hxy; trivial. Qed.
  Next Obligation.
  Proof.
    intros m τi n Δ Δ' HΔ x; cbn;
      destruct lt_dec; try destruct eq_nat_dec; auto.
  Qed.
  Next Obligation.
  Proof.
    intros m n f g Hfg F Δ x; cbn;
      destruct lt_dec; try destruct eq_nat_dec; auto.
  Qed.

  Lemma extend_context_interp_insert (m : nat)
        (τi : leibniz_val -n> iPropG lang Σ)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
        (Ti : leibniz_val -n> iPropG lang Σ)
    :
      (extend_context_interp Ti (context_interp_insert m τi Δ))
         (context_interp_insert (S m) τi (extend_context_interp Ti Δ)).
  Proof.
    intros [|v]; cbn; trivial.
    repeat destruct lt_dec; trivial;
      repeat destruct eq_nat_dec; cbn; auto with omega.
    destruct v; cbn; auto with omega.
    replace (v - 0) with v by omega; trivial.
  Qed.

  Lemma context_interp_insert_O_extend
        (τi : leibniz_val -n> iPropG lang Σ)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
    :
      (context_interp_insert O τi Δ)
         (extend_context_interp τi Δ).
  Proof.
    intros [|v]; cbn; trivial.
    repeat destruct lt_dec; trivial;
      repeat destruct eq_nat_dec; cbn; auto with omega.
    destruct v; cbn; auto with omega.
  Qed.

  Lemma iter_up_subst_type (m : nat) (τ : type) (x : var) :
      (iter m up (τ .: ids) x) =
      if lt_dec x m then ids x else
        if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
  Proof.
    revert x τ.
    induction m; intros x τ; cbn.
    - destruct x; cbn.
      + destruct eq_nat_dec; auto with omega.
        asimpl; trivial.
      + destruct eq_nat_dec; auto with omega.
    - destruct x; asimpl; trivial.
      rewrite IHm.
      repeat destruct lt_dec; repeat destruct eq_nat_dec;
        asimpl; auto with omega.
537
538
539
  Qed.

  Lemma interp_subst_iter_up
540
541
        (m : nat)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
542
        (τ : type)
543
544
545
        (τ' : type)
    : interp τ (context_interp_insert m (interp τ'.[ren (+m)] Δ) Δ)
              interp τ.[iter m up (τ' .: ids)] Δ.
546
  Proof.
547
548
549
550
551
552
553
554
555
556
557
558
    revert m Δ.
    induction τ; intros m Δ v; cbn -[extend_context_interp]; auto.
    - properness; trivial; try apply IHτ1; try apply IHτ2.
    - properness; trivial; try apply IHτ1; try apply IHτ2.
    - properness; trivial; try apply IHτ1; try apply IHτ2.
    - match goal with
        |- _ _ ?f ?x  _ _ ?g ?x =>
        assert (f  g) as Hfg; [|rewrite Hfg; trivial]
      end.
      apply fixpoint_proper => ??; cbn -[extend_context_interp].
      properness; trivial.
      rewrite extend_context_interp_insert.
559
      change (up (iter m up (τ' .: ids))) with (iter (S m) up (τ' .: ids)).
560
561
562
563
564
565
566
567
      rewrite -IHτ.
      replace (τ'.[ren (+S m)]) with ((τ'.[ren (+m)]).[ren (+1)]) by (asimpl; trivial).
      rewrite -interp_ren_S; trivial.
    - rewrite iter_up_subst_type.
      repeat destruct lt_dec; repeat destruct eq_nat_dec;
        unfold ids; asimpl; trivial.
    - properness; trivial.
      rewrite extend_context_interp_insert.
568
      change (up (iter m up (τ' .: ids))) with (iter (S m) up (τ' .: ids)).
569
570
571
572
      rewrite -IHτ.
      replace (τ'.[ren (+S m)]) with ((τ'.[ren (+m)]).[ren (+1)]) by (asimpl; trivial).
      rewrite -interp_ren_S; trivial.
    - properness; trivial; try apply IHτ; trivial.
573
574
575
  Qed.

  Lemma interp_subst
576
577
578
579
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
        (τ : type)
        (τ' : type)
    : interp τ (extend_context_interp (interp τ' Δ) Δ)  interp τ.[τ'/] Δ.
580
  Proof.
581
582
583
    rewrite -(interp_subst_iter_up O Δ τ τ').
    rewrite context_interp_insert_O_extend.
    asimpl; trivial.
584
585
  Qed.

586
587
588
589
590
591
  Lemma zip_with_context_interp_subst
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ) (Γ : list type)
        (vs : list leibniz_val) (τi : leibniz_val -n> iPropG lang Σ) :
    ((Π∧ zip_with (λ τ v, interp τ Δ v) Γ vs)%I)
       (Π∧ zip_with (λ τ v, interp τ (extend_context_interp τi Δ) v)
                    (map (λ t : type, t.[ren (+1)]) Γ) vs)%I.
592
  Proof.
593
594
    revert Δ vs τi.
    induction Γ as [|Γ]; intros Δ vs τi; cbn; trivial.
595
596
597
598
599
600
601
    destruct vs; cbn; trivial.
    apply and_proper.
    - apply interp_ren_S.
    - apply IHΓ.
  Qed.

End logrel.