Commit 8ba734aa authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Compat with Coq 8.8

parent e39352ce
......@@ -198,7 +198,7 @@ Proof.
destruct predsymbs; [|easy].
case eqb; [|easy].
rewrite forallb_map. apply forallb_ext. intros x _.
apply tclosure_check.
apply (tclosure_check G).
- now rewrite IHA1, IHA2.
Qed.
......@@ -207,7 +207,7 @@ Lemma fclosure_level G A :
Proof.
induction A; cbn; auto.
revert l. induction l as [|t l IH]; cbn; auto.
f_equal; auto. apply tclosure_level.
f_equal; auto. apply (tclosure_level G).
Qed.
Lemma fclosure_fclosed G A :
......@@ -405,7 +405,7 @@ Proof.
rewrite Thm_Not in Thm by (apply fclosure_wc; auto).
rewrite <- IH in Thm; auto.
rewrite <- finterp_bsubst0 in Thm; auto. destruct Thm. apply H.
* cbn. apply Thm_NotExNot; auto. apply (fclosure_wc _ (A)); auto.
* cbn. apply Thm_NotExNot; auto. apply (fclosure_wc G (A)); auto.
+ intros Thm (t,Ht).
rewrite finterp_bsubst0 with (u:=t); auto.
2:{ apply term_wc_iff in Ht. apply Ht. }
......@@ -429,7 +429,7 @@ Proof.
rewrite IH in Int; auto.
* rewrite fclosure_bsubst in Int by apply Ht.
apply Thm_Ex_i with t; auto.
apply (fclosure_wc _ (A)); auto.
apply (fclosure_wc G (A)); auto.
* apply bsubst_WF; auto. apply Ht.
+ intros Thm.
destruct (witsat (closure G A) Thm) as (c & Hc & Thm').
......
......@@ -136,8 +136,8 @@ Lemma finterp_ext G L G' L' A :
finterp G L A <-> finterp G' L' A.
Proof.
revert L L'.
induction A; cbn; intros L L' EG EL;
apply interp_quant || f_equiv; auto with set.
induction A; intros L L' EG EL; try apply (interp_quant q);
cbn in *; f_equiv; auto with set.
- apply map_ext_in.
intros a Ha. apply tinterp_ext; eauto with set.
intros k LT. apply EL. apply Nat.lt_le_trans with (level a); auto.
......@@ -194,11 +194,10 @@ Qed.
Lemma finterp_lift G L A n :
finterp G L (lift n A) <-> finterp G (list_drop n L) A.
Proof.
revert n L; induction A; cbn; intros; auto; try easy.
- f_equiv. rewrite map_map. apply map_ext; auto using tinterp_lift.
- f_equiv; auto.
- f_equiv; auto.
- apply interp_quant. intros m. apply IHA.
revert n L; induction A; intros; try apply interp_quant;
cbn; f_equiv; try easy.
- rewrite map_map. apply map_ext; auto using tinterp_lift.
- intros m; apply IHA.
Qed.
Lemma tinterp_bsubst_gen G L L' u m n t :
......@@ -241,12 +240,10 @@ Lemma finterp_bsubst_gen G L L' u m n A :
finterp G L (bsubst n u A) <-> finterp G L' A.
Proof.
revert n u L L'.
induction A; cbn; auto; intros; f_equal; auto; try reflexivity.
- f_equiv. rewrite map_map. apply map_ext. intros a.
induction A; intros; try apply interp_quant; cbn in *; f_equiv; auto; try easy.
- rewrite map_map. apply map_ext. intros a.
eapply tinterp_bsubst_gen; eauto.
- f_equiv; auto.
- f_equiv; auto.
- apply interp_quant. intros m'. apply IHA; auto.
- intros m'; apply IHA; auto.
now rewrite tinterp_lift.
intros [|k]; simpl; auto.
Qed.
......
......@@ -581,7 +581,8 @@ Lemma finterp_zf_congr G L L' A :
finterp preZF G L A <-> finterp preZF G L' A.
Proof.
revert L L'.
induction A; cbn -[EQ]; intros L L' C E; try easy.
induction A; intros L L' C E; try apply interp_quant;
cbn -[EQ] in *; try easy.
- revert C. unfold ZFPreds. unfold predicate_symbol, name in *.
case eqbspec; intros.
+ rewrite lazy_andb_iff in C. destruct C as (C,_).
......@@ -594,7 +595,7 @@ Proof.
f_equiv; apply tinterp_zf_congr; auto.
- f_equiv. auto.
- rewrite lazy_andb_iff in C. destruct C as (C1,C2). f_equiv; auto.
- apply interp_quant. intros m. apply IHA; auto.
- intros m. apply IHA; auto.
intros [|k]; cbn -[EQ]; auto with zfc.
Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment