jak nazwać założenie, pamiętając wyrażenie?

Question

Dokumentacja dla Coq niesie ze sobą ogólne napomnienie , a nie polegać na wbudowanym mechanizmie nazewnictwa, ale wybierz własne nazwy, aby zmiany w mechanizmie nazewnictwa nie uczyniły przeszłych proofów nieważnymi.

Rozważając wyrażenia w formularzu remember Expr as v, ustawiamy zmienną v na wyrażenie Expr. Ale nazwa założeniu jest wybierany automatycznie, a jest coś takiego jak Heqv, więc mamy:

Heqv: v = Expr

Jak mogę wybrać własną nazwę zamiast Heqv? Zawsze mogę zmienić nazwę tego, co lubię, używając polecenia rename, ale to nie zachowuje moich dowodów niezależnych od hipotetycznych przyszłych zmian we wbudowanym mechanizmie nazewnictwa w Coq.

Answer 1

Jeśli możesz pozbyć się oddzielnej równości, spróbuj set (name := val). Użyj unfold zamiast rewrite, aby uzyskać wartość z powrotem na miejscu.

Jeśli potrzebujesz równości dla więcej niż rewrite <-, nie znam żadnej wbudowanej taktyki, która to robi. Możesz to zrobić ręcznie lub zbudować taktykę/notację. Właśnie to zrzuciłem. (Uwaga: nie jestem ekspertem, może to zrobić łatwiej.)

Tactic Notation "remember_as_eq" constr(expr) ident(vname) ident(eqname) := 
    let v  := fresh in 
    let HHelp := fresh in 
    set (v := expr); 
    (assert (HHelp : sigT (fun x => x = v)) by (apply (existT _ v); reflexivity)); 
    inversion HHelp as [vname eqname]; 
    unfold v in *; clear v HHelp; 
    rewrite <- eqname in *. 

Użyj jako remember_as_eq (2+2) four Heqfour aby uzyskać ten sam wynik jak z remember (2+2) as four.

---

Uwaga: Zaktualizowany do obsługi większej liczby przypadków, stara wersja nie powiodła się w przypadku niektórych kombinacji wartości i typu celu. Pozostaw komentarz, jeśli znajdziesz inny przypadek, który działa z rewrite, ale nie ten.