Zulip Chat Archive

You need to help me help you on this one, because it uses some non-standard stuff :). So from looking at the thing, your typ_body is now some L for which K. Then they do pick_freshes? What is that :)? And is poses some variation on pose?

Sean Leather (Apr 24 2018 at 08:22):

You need to help me help you on this one, because it uses some non-standard stuff :smiley:.

Absolutely!

Sean Leather (Apr 24 2018 at 08:23):

pick_freshes is a tactic.

Sean Leather (Apr 24 2018 at 08:23):

poses is another tactic.

Moses Schönfinkel (Apr 24 2018 at 08:23):

Ooh, now it's all clear then!

Sean Leather (Apr 24 2018 at 08:23):

LibTactic.v I believe. I usually grep for it.

Moses Schönfinkel (Apr 24 2018 at 08:23):

Alright, let's see :).

Sean Leather (Apr 24 2018 at 08:24):

What does introv [L K] mean?

Moses Schönfinkel (Apr 24 2018 at 08:24):

It destructs the existential into two parts.

Sean Leather (Apr 24 2018 at 08:24):

Right, thought so.

Moses Schönfinkel (Apr 24 2018 at 08:25):

Your introv [L K] WT basically first intros T Us.

Sean Leather (Apr 24 2018 at 08:25):

And rewrite* and apply* just pull hypotheses from the context, right?

Moses Schönfinkel (Apr 24 2018 at 08:25):

Yes.

Sean Leather (Apr 24 2018 at 08:26):

... which makes it difficult to figure out what's getting used.

Moses Schönfinkel (Apr 24 2018 at 08:26):

Btw, I don't think LibTactics.v has these pick_freshes. It might be coming from something home-baked there?

Moses Schönfinkel (Apr 24 2018 at 08:26):

There's a Metatheory import there, whatever that is.

Sean Leather (Apr 24 2018 at 08:26):

Oh, pick_freshes comes from Metatheory_var.v or Metatheory_fresh.v.

Sean Leather (Apr 24 2018 at 08:27):

Err, or Metatheory_Env.v.

Sean Leather (Apr 24 2018 at 08:28):

Correction: ML_Core_Infrastructure.v.

Sean Leather (Apr 24 2018 at 08:29):

Also, I meant Lib_Tactic.v in this project.

Sean Leather (Apr 24 2018 at 08:30):

pick_fresh and pick_freshes

Sean Leather (Apr 24 2018 at 08:30):

poses

Sean Leather (Apr 24 2018 at 08:32):

I think I get the gist of those. What I'm currently struggling with is what happens to the L and K. Do they get used and how?

Sean Leather (Apr 24 2018 at 08:35):

Because K is a function, right? Something like this out of typ_body:

forall Xs, fresh L n Xs -> type (typ_open_vars T Xs)

Moses Schönfinkel (Apr 24 2018 at 08:35):

pick_fresh and poses don't seem to do anything funny to them, so rewrite* (@typ_substs_intro Xs). apply* typ_substs_types so it's either of these two invocations.

Sean Leather (Apr 24 2018 at 08:35):

I agree.

Moses Schönfinkel (Apr 24 2018 at 08:35):

Yes, K is a function.

Sean Leather (Apr 24 2018 at 08:36):

I think the culprit is typ_substs_intro.

Sean Leather (Apr 24 2018 at 08:37):

Lemma typ_substs_intro : forall Xs Us T,
  fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs ->
  types (length Xs) Us ->
  (typ_open T Us) = typ_substs Xs Us (typ_open_vars T Xs).

Sean Leather (Apr 24 2018 at 08:38):

(So sacrilege: pasting Coq onto a Lean forum...)

Moses Schönfinkel (Apr 24 2018 at 08:40):

Right, so the last apply in the original proof is probably discharging one of the unresolved arguments of rewrites resulting from rewriting typ_subst_intro.

Sean Leather (Apr 24 2018 at 08:40):

(BTW, it would be nice if I could run this. I tried, fixed a few things, but coqc Lib_ListFacts.v doesn't finish in several hours.)

Moses Schönfinkel (Apr 24 2018 at 08:42):

Well that's the overarching problem of reading Coq. (Btw, even rewrite* is non-standard.)

Moses Schönfinkel (Apr 24 2018 at 08:44):

Still, we rewrite (typ_open T Us) with typ_subst Xs Us (typ_open_vars T Xs), we have Xs Us T from rewriting, there should be 2 new obligations, fresh (...) and types .... Either of these may have been discharged by some form of assumption resulting from rewrite*, leaving the last one for the final apply.

Sean Leather (Apr 24 2018 at 08:44):

So my confusion comes down to this (I think): when typ_body is destructed into L and K as forall Xs, fresh L n Xs -> type (typ_open_vars T Xs), is K being used, and, if so, how does fresh L n Xs get instantiated since nothing is known about L?

Moses Schönfinkel (Apr 24 2018 at 08:48):

It doesn't necessarily need to be instantiated for K to still be used.

Moses Schönfinkel (Apr 24 2018 at 08:49):

I don't think the rewrite* or apply* would go beyond defeq or some form of assumption (resulting from the * suffix).

Moses Schönfinkel (Apr 24 2018 at 08:50):

You can still use K to discharge Pi_Xs, _ -> _ which is what I think ends up happening.

Sean Leather (Apr 24 2018 at 08:52):

typ_subst_intro expects fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs. Where does that come from?

Moses Schönfinkel (Apr 24 2018 at 08:54):

It's probably either Fr or Fr', resulting from pick_freshes and assumption'd from the rewrite* call.

Sean Leather (Apr 24 2018 at 08:55):

Ah, right.

Moses Schönfinkel (Apr 24 2018 at 08:56):

apply* typ_substs_types then most likely solves types (length Xs) Us

Moses Schönfinkel (Apr 24 2018 at 08:56):

Can logically K and L help with that? let's see. So they basically map a "parameterized" fresh name to a parameterized type?

Moses Schönfinkel (Apr 24 2018 at 08:58):

It is most likely the case that it's the very last tactic (apply*) that uses K in the Pi form.

Sean Leather (Apr 24 2018 at 08:58):

rewrite* (@typ_substs_intro Xs). apply* typ_substs_types.

Lemma typ_substs_types : forall Xs Us T,
  types (length Xs) Us ->
  type T ->
  type (typ_substs Xs Us T).

Sean Leather (Apr 24 2018 at 08:59):

You can still use K to discharge Pi_Xs, _ -> _ which is what I think ends up happening.

I don't understand this.

Moses Schönfinkel (Apr 24 2018 at 09:02):

It's as you said, there is no reasonable way to instantiate it. So we can just end up assuming the argument comes from someplace.

Moses Schönfinkel (Apr 24 2018 at 09:03):

Aka. the goal transforming to fresh L n Xs -> type (typ_open_vars T Xs) (or fresh L n Xs |- type (...))

Sean Leather (Apr 24 2018 at 09:05):

I'm thinking it would help me to understand poses/pose better.

Sean Leather (Apr 24 2018 at 09:06):

And to figure out where Fr comes from.

Moses Schönfinkel (Apr 24 2018 at 09:06):

I think Fr and Fr' are related to the other hypothesis?

Moses Schönfinkel (Apr 24 2018 at 09:07):

At least if pick_freshes doesn't ever mess with either L or K.

Moses Schönfinkel (Apr 24 2018 at 09:07):

Which it doesn't seem to becasue its argument is a subterm of the other hypothesis (length Us).

Sean Leather (Apr 24 2018 at 09:08):

Ltac pick_freshes_gen L n Y :=
  let Fr := fresh "Fr" in
  let L := beautify_fset L in
  (destruct (var_freshes L n) as [Y Fr]).

Sean Leather (Apr 24 2018 at 09:08):

Does that introduce Fr? It's used by pick_freshes.

Sean Leather (Apr 24 2018 at 09:09):

Oh, and I think pick_freshes/pick_freshes_gen might get L from the assumptions.

Sean Leather (Apr 24 2018 at 09:10):

Via gather_vars.

Sean Leather (Apr 24 2018 at 09:10):

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => {{ x }}) in
  let C := gather_vars_with (fun x : env => dom x) in
  let D := gather_vars_with (fun x : trm => trm_fv x) in
  let E := gather_vars_with (fun x : typ => typ_fv x) in
  let F := gather_vars_with (fun x : list typ => typ_fv_list x) in
  let G := gather_vars_with (fun x : env => env_fv x) in
  let H := gather_vars_with (fun x : sch => sch_fv x) in
  constr:(A \u B \u C \u D \u E \u F \u G \u H).

Sean Leather (Apr 24 2018 at 09:11):

I suppose the gather_vars tactic could also be getting something from K.

Sean Leather (Apr 24 2018 at 09:14):

Right, so Fr comes from pick_freshes and includes L in the free variable finite set.

Moses Schönfinkel (Apr 24 2018 at 09:15):

1) pose introduces h := t : T, a bit like let in lean. poses is their homebrew thing for transforming the introduced h into h : T without t.

Sean Leather (Apr 24 2018 at 09:17):

I think the K obligation of fresh L n Xs could be satisfied by Fr by narrowing down the union of finite sets to extract only L.

Sean Leather (Apr 24 2018 at 09:17):

... the finite set created by gather_vars, which scours the assumptions for variables.

Moses Schönfinkel (Apr 24 2018 at 09:18):

Wouldn't that require something more magical than what rewrite* or apply* can do?

Sean Leather (Apr 24 2018 at 09:18):

Yes.

Sean Leather (Apr 24 2018 at 09:19):

There are other tactics that do that, but, to think of it, they're not being used here, are they?

Sean Leather (Apr 24 2018 at 09:19):

Other homemade tactics, I mean.

Sean Leather (Apr 24 2018 at 09:19):

So maybe I'm jumping ahead of myself.

Moses Schönfinkel (Apr 24 2018 at 09:19):

Right, so here's the thing.

Moses Schönfinkel (Apr 24 2018 at 09:20):

poses Fr' Fr.
rewrite (fresh_length _ _ _  Fr) in WT, Fr'.
rewrite* (@typ_substs_intro Xs). apply* typ_substs_types

Moses Schönfinkel (Apr 24 2018 at 09:20):

The only non-standard one is poses which doesn't do much beyond pose (according to its definition).

Moses Schönfinkel (Apr 24 2018 at 09:21):

rewrite(*) and apply* are standard in the sense that they cannot call anything magical.

Moses Schönfinkel (Apr 24 2018 at 09:22):

The only remaining tactic is pick_freshes (length Us) Xs which can order you a pizza for what we know.

Sean Leather (Apr 24 2018 at 09:22):

Well, I have a vague understanding of what pick_freshes does. It looks at all of the assumptions and picks out all the vars it can find, so that it can choose a free variable not in the resultant finite set of vars.

Sean Leather (Apr 24 2018 at 09:23):

And, if I understand fresh "Fr" correctly, pick_freshes is creating the assumption Fr, which is later used by poses.

Moses Schönfinkel (Apr 24 2018 at 09:25):

Right. Let's say you have p : Prop. pose p then introduces P := p : Prop. poses p also calls clearbody P which gives you p, P : Prop in the context.

Sean Leather (Apr 24 2018 at 09:27):

rewrite (fresh_length _ _ _  Fr) in WT, Fr'.

Lemma fresh_length : forall xs L n, fresh L n xs -> n = length xs.

Moses Schönfinkel (Apr 24 2018 at 09:28):

Right, this fully applies fresh_length so you have n = length xs, you make this rewrite in both WT and Fr'.

Sean Leather (Apr 24 2018 at 09:29):

Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) :=
  n = length L /\ list_forall P L.

 Definition types := list_for_n type.

Sean Leather (Apr 24 2018 at 09:29):

That's where the rewritten length assumptions are used, I believe.

Sean Leather (Apr 24 2018 at 09:29):

That = types.

Sean Leather (Apr 24 2018 at 09:30):

As in here:

Lemma typ_substs_intro : forall Xs Us T,
  fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs ->
  types (length Xs) Us ->
  (typ_open T Us) = typ_substs Xs Us (typ_open_vars T Xs).

Moses Schönfinkel (Apr 24 2018 at 09:31):

types is simple enough then, it's a filtered vector, conceptually

Moses Schönfinkel (Apr 24 2018 at 09:35):

typ_substs_types however is _ -> type (typ_substs Xs Us T), so there's no way for apply* to resolve types with it

Moses Schönfinkel (Apr 24 2018 at 09:36):

So I was wrong wrt. what the last apply* pertains to it seems.

Sean Leather (Apr 24 2018 at 09:38):

Yes, I think so. After rewrite* (@typ_substs_intro ...), you get type (typ_substs ...) in the goal.

Moses Schönfinkel (Apr 24 2018 at 09:38):

Right, so that one is magically discharged.

Sean Leather (Apr 24 2018 at 09:38):

... which is fulfilled by apply* typ_substs_types

Sean Leather (Apr 24 2018 at 09:41):

Are you sure there isn't more magic being done by rewrite* and/or apply*? Do those use the Hints that are all over the place in this project?

Sean Leather (Apr 24 2018 at 09:41):

$ git grep Hint | wc -l
     204

Sean Leather (Apr 24 2018 at 09:49):

@Moses Schönfinkel I have to go prepare lunch and feed my kid. Sorry. I'll be back on later. Feel free to leave any insightful and illuminating thoughts here for me to read upon my return. :smile:

Kevin Buzzard (Apr 24 2018 at 09:58):

I'm sure the moderators will have shut this thread down by then ;-)

Moses Schönfinkel (Apr 24 2018 at 10:06):

Can / should I migrate this to a separate stream? @Kevin Buzzard

Moses Schönfinkel (Apr 24 2018 at 10:07):

For example maths is this completely random topic that few here care about and has its own stream.. errrm :).

Kevin Buzzard (Apr 24 2018 at 10:08):

:-) I have no idea -- as I'm sure you are aware, I was not being remotely serious.

Moses Schönfinkel (Apr 24 2018 at 10:13):

@Sean Leather I'll take a closer look when I get home, I have some teaching to do

Sean Leather (Apr 24 2018 at 10:57):

Thanks. Lunch is over. I'll continue looking at it in the meantime, at least until the moderators or Kevin shut me down. If that happens, I'm sure I'll lose my mind, since I will no longer be able to voice my confusion publicly. :poop:

Sean Leather (Apr 24 2018 at 11:28):

Annotated:

Lemma typ_open_types : forall T Us,
  typ_body (length Us) T ->

Definition typ_body n T := exists L, forall Xs, fresh L n Xs -> type (typ_open_vars T Xs).

  types (length Us) Us ->

Definition types := list_for_n type.

Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) := n = length L /\ list_forall P L.

  type (typ_open T Us).
Proof.
  introv [L K] WT.

L : vars (a.k.a. FinSet)

K : forall Xs, fresh L n Xs -> type (typ_open_vars T Xs)

  pick_freshes (length Us) Xs.

Creates an assumption named Fr defined as the union of all finite sets of variables in the context for some list. That is, I think Fr : fresh L (length Us) Xs because destruct (var_freshes L n) as [Y Fr] and Lemma var_freshes : forall L n, { xs : list var | fresh L n xs }.

  poses Fr' Fr.

Copies Fr to Fr'.

  rewrite (fresh_length _ _ _  Fr) in WT, Fr'.

Lemma fresh_length : forall xs L n, fresh L n xs -> n = length xs.

  rewrite* (@typ_substs_intro Xs).

Lemma typ_substs_intro : forall Xs Us T, fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs -> types (length Xs) Us -> (typ_open T Us) = typ_substs Xs Us (typ_open_vars T Xs).

  apply* typ_substs_types.

Lemma typ_substs_types : forall Xs Us T, types (length Xs) Us -> type T -> type (typ_substs Xs Us T).

Qed.

Sean Leather (Apr 24 2018 at 11:57):

See https://gist.github.com/spl/a204842b476cc46fb1b879ee2baedfbd for an easier-to-read and updated version of the above.

Sean Leather (Apr 24 2018 at 12:17):

Okay, I believe I have a better handle on what's going on.

Sean Leather (Apr 24 2018 at 12:17):

I've found where L and K are used.

Sean Leather (Apr 24 2018 at 12:18):

There is definitely more magic being applied here than meets the eye.

Sean Leather (Apr 24 2018 at 12:19):

I believe the fresh properties are being manipulated into their expected forms using the magic in Metatheory_Fresh.v.

Sean Leather (Apr 24 2018 at 12:20):

I couldn't explain the technical mechanism, but I believe it has to do with all the Hints to get certain tactics to perform automagically.

Sean Leather (Apr 24 2018 at 12:20):

In particular, for fresh, it's:

Metatheory_Fresh.v:Hint Extern 1 (fresh _ _ _) => fresh_solve.

Sean Leather (Apr 24 2018 at 12:24):

Also, there's this dark magic underlying pick_freshes:

(** [gather_vars_with F] return the union of all the finite sets
  of variables [F x] where [x] is a variable from the context such that
  [F x] type checks. In other words [x] has to be of the type of the
  argument of [F]. The resulting union of sets does not contain any
  duplicated item. This tactic is an extreme piece of hacking necessary
  because the tactic language does not support a "fold" operation on
  the context. *)

Sean Leather (Apr 24 2018 at 12:25):

Used as so:

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => {{ x }}) in
  let C := gather_vars_with (fun x : env => dom x) in
  let D := gather_vars_with (fun x : trm => trm_fv x) in
  let E := gather_vars_with (fun x : typ => typ_fv x) in
  let F := gather_vars_with (fun x : list typ => typ_fv_list x) in
  let G := gather_vars_with (fun x : env => env_fv x) in
  let H := gather_vars_with (fun x : sch => sch_fv x) in
  constr:(A \u B \u C \u D \u E \u F \u G \u H).

Sean Leather (Apr 24 2018 at 12:26):

And (it just clicked for me) that is how typ_fv and typ_fv_list are appearing.

Moses Schönfinkel (Apr 25 2018 at 06:51):

Sorry I didn't manage to get around to using my computer yesterday! :(

Sean Leather (Apr 25 2018 at 07:00):

I progressed a bit further, as you can see. I'm slightly better at systematically reverse engineering Coq proofs now. Thanks for that! :simple_smile:

Moses Schönfinkel (Apr 25 2018 at 07:09):

What a wonderful world this would be if you could run it :-\.

Sean Leather (Apr 25 2018 at 07:24):

I've reverted to working on my Lean version of this proof. I have an idea of how to do the part of the fresh manipulation that is implemented with hidden dark magic in Coq, and I'm trying to work it out, in Lean, without magic.

Moses Schönfinkel (Apr 25 2018 at 07:30):

You can also try Lean, with magic.

Sean Leather (Apr 25 2018 at 07:31):

You mean, by writing tactics? I've avoided that so far, just so I can get a handle on how to do the proofs.

Moses Schönfinkel (Apr 25 2018 at 07:34):

Yeah. I'm not entirely sure how useful learning it would be as of right now, given Lean 4 might (will?) change that.

Sean Leather (Apr 25 2018 at 07:38):

That unknown future always seems to hang in the air, doesn't it? The possibility of change infects one's thoughts.

Sean Leather (Apr 25 2018 at 07:41):

Apparently, Coq has changed a lot over the years, too. This project was supposed to work with 8.1, and now, with 8.8, it just compiles for more hours than I've been willing to wait.

Kevin Buzzard (Apr 25 2018 at 07:42):

When mathematicians hear talks about the great things that have been achieved using computer proof checkers

Kevin Buzzard (Apr 25 2018 at 07:42):

then the odd order theorem is always mentioned as one of the jewels in the crown

Kevin Buzzard (Apr 25 2018 at 07:43):

(before Kepler it was _the_ jewel)

Kevin Buzzard (Apr 25 2018 at 07:43):

and apparently that no longer compiles in Coq current

Kevin Buzzard (Apr 25 2018 at 07:43):

so I have heard

Kevin Buzzard (Apr 25 2018 at 07:43):

if either if you are in a position to formally verify this rumour I'd appreciate it

Sean Leather (Apr 25 2018 at 07:45):

https://github.com/math-comp/odd-order is 8 days old. Maybe it's an update.

Sean Leather (Apr 25 2018 at 07:46):

Anyway, that's what I got from the first page of a Google search. :simple_smile:

Johan Commelin (Apr 25 2018 at 07:48):

Hmm, seems like it's working again.

Johan Commelin (Apr 25 2018 at 07:48):

I heard this rumour on the ssreflect mailing list about a year ago

Johan Commelin (Apr 25 2018 at 07:48):

Sounded pretty broken back then

Johan Commelin (Apr 25 2018 at 07:49):

They were talking about distributing the proof with an old version of Coq inside a docker package. Just to make sure people could easily return to a version that compiles.

Johan Commelin (Apr 25 2018 at 07:49):

All the better if it actually compiles with the latest release!

Sean Leather (Apr 25 2018 at 08:03):

They were talking about distributing the proof with an old version of Coq inside a docker package. Just to make sure people could easily return to a version that compiles.

I just discovered https://github.com/proofengineering/coq-docker

Sean Leather (Apr 25 2018 at 09:31):

Et voilà! I just figured out how to install Coq 8.1 and built the Coq project. :hatching_chick:

Kevin Buzzard (Apr 25 2018 at 09:36):

They occasionally prove false in Coq, right? And then of course things get patched. Do the patches extend back as far as things like 8.1? I know that this might all sound trivial to CS people but mathematicians, who are still in my view extremely skeptical about this formal proof verification thing, are not going to be too impressed by "proof of odd order theorem in a system which can also prove anything".

Kevin Buzzard (Apr 25 2018 at 09:37):

https://github.com/clarus/falso

Kevin Buzzard (Apr 25 2018 at 09:37):

8.1 < 8.4.6

Mario Carneiro (Apr 25 2018 at 09:37):

which can also prove anything

only on tuesdays

Kevin Buzzard (Apr 25 2018 at 09:38):

only if you use a type with 256 constructors

Sean Leather (Apr 25 2018 at 09:40):

For my purpose, I'm just trying to figure out what some Coq proof does and translate that to Lean. So, since we never prove false in Lean, there shouldn't be any problem, right?

Kevin Buzzard (Apr 25 2018 at 09:41):

I guess so!

Sean Leather (Apr 25 2018 at 10:06):

Great. I can walk through the proof in CoqIde now. But it doesn't show the magic happening behind the scenes.

Sean Leather (Apr 25 2018 at 10:09):

Oh, but I can remove the * from rewrite* to see the subgoals. :light_bulb:

Moses Schönfinkel (Apr 25 2018 at 11:13):

@Kevin Buzzard Remember you also can't trust that pesky hardware Lean runs on!

Sean Leather (Apr 25 2018 at 11:55):

And... my Coq woes are over! I have successfully translated this particular Coq proof into Lean. :raised_hands:

Last updated: Dec 20 2023 at 11:08 UTC