Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Take relevance into account for typing #1101

Open
wants to merge 1 commit into
base: coq-8.19
Choose a base branch
from
+1,529 −1,017
Open

Take relevance into account for typing #1101

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 21 additions & 13 deletions common/theories/BasicAst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,10 @@ Lemma map_dbody {A B} (f : A -> B) (g : A -> B) (d : def A) :
g (dbody d) = dbody (map_def f g d).
Proof. destruct d; reflexivity. Qed.

Lemma map_dname {A B} (f : A -> B) (g : A -> B) (d : def A) :
dname d = dname (map_def f g d).
Proof. destruct d; reflexivity. Qed.

Definition mfixpoint term := list (def term).

Definition test_def {A} (tyf bodyf : A -> bool) (d : def A) :=
Expand Down Expand Up @@ -217,13 +221,13 @@ Record judgment_ {universe Term} := Judge {
j_term : option Term;
j_typ : Term;
j_univ : option universe;
(* j_rel : option relevance; *)
j_rel : option relevance;
}.
Arguments judgment_ : clear implicits.
Arguments Judge {universe Term} _ _ _.

Definition judgment_map {univ T A} (f: T -> A) (j : judgment_ univ T) :=
Judge (option_map f (j_term j)) (f (j_typ j)) (j_univ j) (* (j_rel j) *).
Judge (option_map f (j_term j)) (f (j_typ j)) (j_univ j) (j_rel j).

Section Contexts.
Context {term : Type}.
Expand All @@ -239,17 +243,21 @@ End Contexts.

Arguments context_decl : clear implicits.

Notation Typ typ := (Judge None typ None).
Notation TermTyp tm ty := (Judge (Some tm) ty None).
Notation TermoptTyp tm typ := (Judge tm typ None).
Notation TypUniv ty u := (Judge None ty (Some u)).
Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u)).

Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)) (only parsing).
Notation j_vass_s na ty s := (TypUniv ty s (* na.(binder_relevance) *)) (only parsing).
Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)) (only parsing).
Notation j_decl d := (TermoptTyp (decl_body d) (decl_type d) (* (decl_name d).(binder_relevance) *)).
Notation j_decl_s d s := (Judge (decl_body d) (decl_type d) s (* (decl_name d).(binder_relevance) *)).
Notation Typ typ := (Judge None typ None None).
Notation TypRel typ rel := (Judge None typ None (Some rel)).
Notation TermTyp tm ty := (Judge (Some tm) ty None None).
Notation TermTypRel tm ty rel := (Judge (Some tm) ty None (Some rel)).
Notation TermoptTyp tm typ := (Judge tm typ None None).
Notation TermoptTypRel tm typ rel := (Judge tm typ None (Some rel)).
Notation TypUniv ty u := (Judge None ty (Some u) None).
Notation TypUnivRel ty u rel := (Judge None ty (Some u) (Some rel)).
Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u) None).

Notation j_vass na ty := (TypRel ty na.(binder_relevance)).
Notation j_vass_s na ty s := (TypUnivRel ty s na.(binder_relevance)).
Notation j_vdef na b ty := (TermTypRel b ty na.(binder_relevance)).
Notation j_decl d := (TermoptTypRel (decl_body d) (decl_type d) (decl_name d).(binder_relevance)).
Notation j_decl_s d s := (Judge (decl_body d) (decl_type d) s (Some (decl_name d).(binder_relevance))).

Definition map_decl {term term'} (f : term -> term') (d : context_decl term) : context_decl term' :=
{| decl_name := d.(decl_name);
Expand Down
24 changes: 22 additions & 2 deletions common/theories/Environment.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,8 @@ Module Environment (T : Term).
(** Local (de Bruijn) context *)

Definition context := list context_decl.
Definition mark_context := list relevance.
Definition marks_of_context : context -> mark_context := fun l => List.map (fun d => d.(decl_name).(binder_relevance)) l.

(** Last declaration first *)

Expand Down Expand Up @@ -850,7 +852,7 @@ Module Environment (T : Term).
end.

Definition tImpl (dom codom : term) : term :=
tProd {| binder_name := nAnon; binder_relevance := Relevant |}
tProd {| binder_name := nAnon; binder_relevance := rel_of_Type |}
dom (lift 1 0 codom).

Definition array_uctx := ([nAnon], ConstraintSet.empty).
Expand Down Expand Up @@ -998,12 +1000,30 @@ Module Environment (T : Term).

Definition arities_context (l : list one_inductive_body) :=
rev_map (fun ind => vass (mkBindAnn (nNamed ind.(ind_name))
(ind.(ind_relevance))) ind.(ind_type)) l.
rel_of_Type) ind.(ind_type)) l.

Lemma arities_context_length l : #|arities_context l| = #|l|.
Proof. unfold arities_context. now rewrite rev_map_length. Qed.
#[global] Hint Rewrite arities_context_length : len.

Lemma nth_error_arities_context idecls i idecl :
nth_error (List.rev idecls) i = Some idecl ->
nth_error (arities_context idecls) i =
Some {| decl_name := {| binder_name := nNamed idecl.(ind_name); binder_relevance := rel_of_Type |};
decl_body := None;
decl_type := idecl.(ind_type) |}.
Proof using Type.
intros hnth.
epose proof (nth_error_Some_length hnth). autorewrite with len in H.
rewrite nth_error_rev in hnth. now autorewrite with len.
rewrite List.rev_involutive in hnth. autorewrite with len in hnth.
unfold arities_context.
rewrite rev_map_spec.
rewrite nth_error_rev; autorewrite with len; auto.
rewrite List.rev_involutive nth_error_map.
rewrite hnth. simpl. reflexivity.
Qed.

Definition map_mutual_inductive_body f m :=
match m with
| Build_mutual_inductive_body finite ind_npars ind_pars ind_bodies ind_universes ind_variance =>
Expand Down
Loading
Loading