logrel.v 20.9 KB
Newer Older
1
2
3
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
4
5
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
        iris_logrel.F_mu_ref.rules.
6
7
8
9
10
11
12
13
14
15
16
17
18
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.

19
  Canonical Structure leibniz_var := leibnizC var.
20

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
  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
37
38
    |}.

39
40
41
42
  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 Σ) :=
43
    {|
44
      cofe_mor_car := λ f, extend_context_interp_fun1 τi f
45
    |}.
46
47
  Next Obligation.
  Proof. intros ???? Hfg x; destruct x; cbn; trivial. Qed.
48

49
50
51
52
  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 Σ) :=
53
    {|
54
      cofe_mor_car := λ τi, extend_context_interp_fun2 τi
55
    |}.
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
  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.
77
  Proof.
78
79
80
81
82
83
84
    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.
85
86
  Qed.

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

92
93
94
  Program Definition interp_prod :
    (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ) -n>
    leibniz_val -n> iPropG lang Σ :=
95
96
    {|
      cofe_mor_car :=
97
98
99
100
101
102
        λ τ1i,
        {|
          cofe_mor_car :=
            λ τ2i,
            {|
              cofe_mor_car :=
103
                λ w, ( w1 w2, w = PairV w1 w2  τ1i w1  τ2i w2)%I
104
105
            |}
        |}
106
    |}.
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
  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 :=
123
124
                λ w, (( w1, w = InjLV w1  τ1i w1) 
                      ( w2, w = InjRV w2  τ2i w2))%I
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
            |}
        |}
    |}.
  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 :=
144
                λ w, (  v, τ1i v  WP (App (# w) (# v)) @  {{τ2i}})%I
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
            |}
        |}
    |}.
  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,
164
165
166
            ( (τ'i : {f : (leibniz_val -n> iPropG lang Σ) |
                       Val_to_IProp_Persistent f}),
                 (WP TApp (# w) @  {{λ v, (τi (`τ'i) v)}}))%I
167
168
169
        |}
    |}.
  Next Obligation.
170
  Proof.
171
    intros τ τ' x y Hxy; cbn; rewrite Hxy; trivial.
172
  Qed.
173
  Next Obligation.
174
    intros n f g Hfg x; cbn.
175
    apply forall_ne=> P.
176
    apply always_ne, wp_ne => w.
177
    rewrite Hfg; trivial.
178
179
  Qed.

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

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

220
221
222
223
224
225
226
227
228
  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.
229
230
231
232

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

233
234
235
236
237
238
239
  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.
240

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

258
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
  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)
289
    : PersistentP (f v).
290
  Proof. apply Hf. Qed.
291
292
293
294
295

  Global Instance interp_Persistent
         τ (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
         {HΔ : context_interp_Persistent Δ}
    : Val_to_IProp_Persistent (interp τ Δ).
296
  Proof.
297
298
299
300
301
    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Δ.
302
303
  Qed.

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

309
310
311
312
313
314
315
  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Δ.
316
317
  Qed.

318
  Local Ltac properness :=
319
320
    repeat
      match goal with
321
322
323
324
325
326
327
328
329
330
      | |- ( _: _, _)%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
331
332
      end.

333
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
  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.
381

382
383
384
385
386
387
388
389
390
391
392
393
394
  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.
395

396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
  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.
414
415

  Lemma interp_subst_weaken
416
417
        (m n : nat)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
418
        (τ : type)
419
    : interp τ Δ  interp τ.[iter m up (ren (+n))] (hop_context_interp m n Δ).
420
  Proof.
421
422
423
424
425
426
427
428
429
430
431
432
    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τ.
433
      change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
434
435
436
437
438
439
440
441
442
443
444
445
446
      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.
447
      change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
448
449
450
451
      rewrite IHτ.
      apply interp_unused_contex_irrel.
      intros w; rewrite extend_bofore_hop_context_interp; trivial.
    - properness; trivial; try apply IHτ; trivial.
452
453
  Qed.

454
455
  Lemma interp_ren_S (τ : type)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
456
        (τi : leibniz_val -n> iPropG lang Σ)
457
    : interp τ Δ  interp τ.[ren (+1)] (extend_context_interp τi Δ).
458
  Proof.
459
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
    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.
536
537
538
  Qed.

  Lemma interp_subst_iter_up
539
540
        (m : nat)
        (Δ : leibniz_var -n> leibniz_val -n> iPropG lang Σ)
541
        (τ : type)
542
543
544
        (τ' : type)
    : interp τ (context_interp_insert m (interp τ'.[ren (+m)] Δ) Δ)
              interp τ.[iter m up (τ' .: ids)] Δ.
545
  Proof.
546
547
548
549
550
551
552
553
554
555
556
557
    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.
558
      change (up (iter m up (τ' .: ids))) with (iter (S m) up (τ' .: ids)).
559
560
561
562
563
564
565
566
      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.
567
      change (up (iter m up (τ' .: ids))) with (iter (S m) up (τ' .: ids)).
568
569
570
571
      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.
572
573
574
  Qed.

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

585
586
587
588
589
590
  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.
591
  Proof.
592
593
    revert Δ vs τi.
    induction Γ as [|Γ]; intros Δ vs τi; cbn; trivial.
594
595
596
597
598
599
600
    destruct vs; cbn; trivial.
    apply and_proper.
    - apply interp_ren_S.
    - apply IHΓ.
  Qed.

End logrel.