(****************************************************************
Copyright © 2010-2024 Amy Felty
This file is part of "Two-Level Hybrid in Coq"
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see .
***************************************************************)
(****************************************************************
File: ShapesG.v
original: January 2010
updated: March 2014
Apr 2024: Current Coq Version: V8.18.0
Generalized context version (G version) of
proofs of properties about equality and shapes.
***************************************************************)
From HybridSys Require Export Shapes.
(****************************************************************
1. If equal T E then shape T E.
****************************************************************)
Section eqsh.
(************)
(* Contexts *)
(************)
Inductive avG : list atm -> Prop :=
| nil_av: avG nil
| cons_av: forall (Phi:list atm) (x y:uexp), proper x -> proper y ->
avG Phi -> avG (eq_a x y::varE y::varT x::Phi).
Hint Resolve nil_av cons_av : hybrid.
Lemma memb_av : forall (Phi:list atm) (x y:uexp),
avG Phi -> In (eq_a x y) Phi ->
(In (varT x) Phi /\ In (varE y) Phi).
Proof.
intros Phi x y; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | [h2 | [h2 | h2]]].
- injection h2; intros; subst; simpl; auto.
- discriminate h2.
- discriminate h2.
- simpl; tauto.
Qed.
Lemma shape_strengthen_weaken :
forall (i:nat) (T E:uexp) (Phi Psi:list atm),
(forall (T:uexp), In (varT T) Phi <-> In (varT T) Psi) ->
(forall (E:uexp), In (varE E) Phi <-> In (varE E) Psi) ->
(forall (T E:uexp), In (shape T E) Phi <-> In (shape T E) Psi) ->
seq_ i Phi (atom_ (shape T E)) ->
seq_ i Psi (atom_ (shape T E)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (T E:uexp) (Phi Psi:list atm),
(forall (T:uexp), In (varT T) Phi <-> In (varT T) Psi) ->
(forall (E:uexp), In (varE E) Phi <-> In (varE E) Psi) ->
(forall (T E:uexp), In (shape T E) Phi <-> In (shape T E) Psi) ->
seq_ i Phi (atom_ (shape T E)) ->
seq_ i Psi (atom_ (shape T E)))).
intro H'.
apply H'; clear H' i; auto.
intros i h T E Phi Psi h1 h2 h3' h4.
inversion h4; subst; clear h4.
- inversion H0; subst; clear H0.
(* varT/varE case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_;
apply s_bc with (Conj (atom_ (varT T)) (atom_ (varE E)));
eauto with hybrid.
apply s_and; auto.
* inversion H4; subst; clear H4.
-- inversion H0; subst; clear H0.
-- destruct (h1 T) as [h3 h4].
specialize (h3 H2).
generalize h3; clear h3; case Psi; try (simpl; tauto).
intros a l h3; apply s_init; auto.
* inversion H5; subst; clear H5.
-- inversion H0; subst; clear H0.
-- destruct (h2 E) as [h3 h4].
specialize (h3 H2).
generalize h3; clear h3; case Psi; try (simpl; tauto).
intros a l h3; apply s_init; auto.
(* lam case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_;
apply s_bc with
(All (fun x:uexp =>
(All (fun y:uexp =>
(Imp (varT x) (Imp (varE y) (atom_ (shape (T0 x) (E0 y)))))))));
eauto with hybrid.
apply s_all; auto.
intros x h3.
generalize (H4 x h3); clear H4; intro h4.
inversion h4; subst; clear h4.
apply s_all; auto.
intros y h4.
generalize (H3 y h4); clear H3; intro h5.
inversion h5; subst; clear h5.
inversion H3; subst; clear H3.
apply s_imp; auto.
apply s_imp; auto.
apply h with (varE y::varT x::Phi); auto; try lia.
(* proof of extended context inv *)
* intros T; generalize (h1 T); simpl; tauto.
* intros E; generalize (h2 E); simpl; tauto.
* intros T E; generalize (h3' T E); simpl; tauto.
(* app case *)
+ inversion H3; subst; clear H3.
assert (hi:i
seq_ i (varE y::varT x::Gamma) (atom_ (shape T E)).
Proof.
intros i T T' x y Gamma h.
apply shape_strengthen_weaken with (eq_a x y::varE y::varT x::Gamma); auto.
- clear h T T' i.
intros T; simpl; split.
+ intros [h1 | [h1 | [h1 | h1]]]; try discriminate h1; auto.
+ intros [h1 | [h1 | h1]]; try discriminate h1; auto.
- clear h T T' i.
intros E; simpl; split.
+ intros [h1 | [h1 | [h1 | h1]]]; try discriminate h1; auto.
+ intros [h1 | [h1 | h1]]; try discriminate h1; auto.
- clear h T T' i.
intros T E; simpl; split.
+ intros [h1 | [h1 | [h1 | h1]]]; try discriminate h1; auto.
+ intros [h1 | [h1 | h1]]; try discriminate h1; auto.
Qed.
(****************************)
(* Main Lemmas and Theorems *)
(****************************)
Lemma eq_shape :
forall (i:nat) (T E:uexp) (Phi:list atm), avG Phi ->
seq_ i Phi (atom_ (eq_a T E)) ->
seq_ (2*i+2) Phi (atom_ (shape T E)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (T E:uexp) (Phi:list atm), avG Phi ->
seq_ i Phi (atom_ (eq_a T E)) ->
seq_ (2*i+2) Phi (atom_ (shape T E)))).
intro H'.
apply H'; clear H' i; auto.
intros i h T E Phi cInv h1.
inversion h1; subst; clear h1.
- inversion H0; subst; clear H0.
(* lam case *)
+ generalize (eq_lam_inv i0 Phi T0 E0 H3); clear H3; intros [j [h1 h2]];
subst.
replace (2*(j+3+1)+2) with (2*j+1+1+1+1+1+1+1+1+1+1); try lia.
unfold seq_,atom_;
apply s_bc with
(All (fun x:uexp =>
(All (fun y:uexp =>
(Imp (varT x) (Imp (varE y) (atom_ (shape (T0 x) (E0 y)))))))));
auto with hybrid.
apply s_all; auto.
intros x h1.
apply s_all; auto.
intros y h3.
apply s_imp; auto.
apply s_imp; auto.
apply seq_mono with (2*j+2); auto; try lia.
apply d_str_av2v_shape; auto.
apply h; eauto with hybrid; try lia.
apply seq_thin_exch with (eq_a x y::Phi); auto.
* intro a; simpl; tauto.
* apply h2; auto.
(* app case *)
+ inversion H3; subst; clear H3.
replace (2*(i+1+1)+2) with (2*i+1+1+1+1+1+1); try lia.
unfold seq_,atom_;
apply s_bc with (Conj (atom_ (shape T1 E1)) (atom_ (shape T2 E2)));
auto with hybrid.
apply s_and; auto.
* apply seq_mono with (2*i+2); auto; try lia.
apply h; try lia; auto.
* apply seq_mono with (2*i+2); auto; try lia.
apply h; try lia; auto.
(* context case *)
- inversion cInv; subst.
specialize memb_av with (1:=cInv) (2:=H2); intros [h1 h2]; clear H2.
replace (2*i+2) with (2*i+1+1); try lia.
unfold seq_,atom_; apply s_bc with (Conj (atom_ (varT T)) (atom_ (varE E)));
auto with hybrid.
apply s_and; auto.
* apply s_init; auto with hybrid.
* apply s_init; auto with hybrid.
Qed.
Lemma eq_shape_cor : forall (T E:uexp),
seq0 (atom_ (eq_a T E)) -> seq0 (atom_ (shape T E)).
Proof.
intros T E [i h1].
generalize nil_av; intro h2.
specialize eq_shape with (1:=h2) (2:=h1); intro h.
exists (2*i+2); auto.
Qed.
End eqsh.